+
+lemma square_ordered_set: ordered_set → ordered_set.
+intro O;
+apply (mk_ordered_set (O × O));
+[1: intros (x y); apply (\fst x ≰ \fst y ∨ \snd x ≰ \snd y);
+|2: intro x0; cases x0 (x y); clear x0; simplify; intro H;
+ cases H (X X); apply (os_coreflexive ?? X);
+|3: intros 3 (x0 y0 z0); cases x0 (x1 x2); cases y0 (y1 y2) ; cases z0 (z1 z2);
+ clear x0 y0 z0; simplify; intro H; cases H (H1 H1); clear H;
+ [1: cases (os_cotransitive ??? z1 H1); [left; left|right;left]assumption;
+ |2: cases (os_cotransitive ??? z2 H1); [left;right|right;right]assumption]]
+qed.
+
+notation "s 2 \atop \nleq" non associative with precedence 90
+ for @{ 'square_os $s }.
+notation > "s 'square'" non associative with precedence 90
+ for @{ 'square $s }.
+interpretation "ordered set square" 'square s = (square_ordered_set s).
+interpretation "ordered set square" 'square_os s = (square_ordered_set s).
+
+definition os_subset ≝ λO:ordered_set.λP,Q:O→Prop.∀x:O.P x → Q x.
+
+interpretation "ordered set subset" 'subseteq a b = (os_subset _ a b).
+