-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.
+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.