+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.
+
+coercion segment_square_of_ordered_set_square with 0 2 nocomposites.
+
+alias symbol "pi1" (instance 4) = "exT \fst".
+alias symbol "pi1" (instance 2) = "exT \fst".
+lemma ordered_set_square_of_segment_square :
+ ∀O:ordered_set.∀u,v:O.{[u,v]} squareO → O squareO ≝
+ λO:ordered_set.λu,v:O.λb:{[u,v]} squareO.〈\fst(\fst b),\fst(\snd b)〉.
+
+coercion ordered_set_square_of_segment_square nocomposites.