-lemma segment_square_of_O_square:
- ∀O:ordered_set.∀u,v:O.∀x:O square.fst x ∈ [u,v] → snd x ∈ [u,v] → {[u,v]} square.
-intros; split; exists; [1: apply (fst x) |3: apply (snd x)] assumption;
+definition invert_os_relation ≝
+ λC:ordered_set.λU:C square → Prop.
+ λx:C square. U 〈\snd x,\fst x〉.
+
+interpretation "relation invertion" 'invert a = (invert_os_relation _ a).
+interpretation "relation invertion" 'invert_symbol = (invert_os_relation _).
+interpretation "relation invertion" 'invert_appl a x = (invert_os_relation _ a x).
+
+lemma segment_square_of_ordered_set_square:
+ ∀O:ordered_set.∀u,v:O.∀x:O square.
+ \fst x ∈ [u,v] → \snd x ∈ [u,v] → {[u,v]} square.
+intros; split; exists; [1: apply (\fst x) |3: apply (\snd x)] assumption;