lemma orelation_of_relation_preserves_composition:
∀o1,o2,o3:REL.∀F: arrows1 ? o1 o2.∀G: arrows1 ? o2 o3.
orelation_of_relation ?? (G ∘ F) =
lemma orelation_of_relation_preserves_composition:
∀o1,o2,o3:REL.∀F: arrows1 ? o1 o2.∀G: arrows1 ? o2 o3.
orelation_of_relation ?? (G ∘ F) =