lemma ordered_set_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)〉.
lemma ordered_set_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)〉.