-alias symbol "pi1" (instance 4) = "sigma pi1".
-alias symbol "pi1" (instance 2) = "sigma pi1".
-lemma O_square_of_segment_square :
- ∀O:ordered_set.∀u,v:O.{[u,v]} square → O square ≝
- λO:ordered_set.λu,v:O.λb:{[u,v]} square.〈fst(fst b),fst(snd b)〉.
+definition invert_os_relation ≝
+ λC:ordered_set.λU:C squareO → Prop.
+ λx:C squareO. 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 squareO.
+ \fst x ∈ [u,v] → \snd x ∈ [u,v] → {[u,v]} squareO.
+intros; split; exists; [1: apply (\fst x) |3: apply (\snd x)] assumption;
+qed.