- ∀o1,o2,o3:REL.∀F: arrows1 ? o1 o2.∀G: arrows1 ? o2 o3.
- orelation_of_relation ?? (G ∘ F) =
- comp2 OA (SUBSETS o1) (SUBSETS o2) (SUBSETS o3)
- ?? (*(orelation_of_relation ?? F) (orelation_of_relation ?? G)*).
- [ apply (orelation_of_relation ?? F); | apply (orelation_of_relation ?? G); ]
+ ∀o1,o2,o3:REL.∀F: o1 ⇒_\r1 o2.∀G: o2 ⇒_\r1 o3.
+ orelation_of_relation ?? (G ∘ F) =
+ comp2 OA ??? (orelation_of_relation ?? F) (orelation_of_relation ?? G).