+
+notation "'exc_le_variance'" non associative with precedence 90 for @{'exc_le_variance}.
+notation "'exc_ge_variance'" non associative with precedence 90 for @{'exc_ge_variance}.
+
+interpretation "exc_le_variance" 'exc_le_variance = (exc_hle_variance (os_l _)).
+interpretation "exc_ge_variance" 'exc_ge_variance = (exc_hle_variance (os_r _)).
+
+definition square_exc ≝
+ λO:half_ordered_set.λx,y:O×O.\fst x ≰≰ \fst y ∨ \snd x ≰≰ \snd y.
+
+lemma square_half_ordered_set: half_ordered_set → half_ordered_set.
+intro O;
+apply (mk_half_ordered_set (O × O));
+[1: apply (wloss O);
+|2: intros; cases (wloss_prop O); [left|right] intros; apply H;
+|3: apply (square_exc O);
+|4: intro x; cases (wloss_prop O); rewrite < (H ?? (square_exc O) x x); clear H;
+ cases x; clear x; unfold square_exc; intro H; cases H; clear H; simplify in H1;
+ [1,3: apply (hos_coreflexive O h H1);
+ |*: apply (hos_coreflexive O h1 H1);]
+|5: intros 3 (x0 y0 z0); cases (wloss_prop O);
+ do 3 rewrite < (H ?? (square_exc O)); clear H; cases x0; cases y0; cases z0; clear x0 y0 z0;
+ simplify; intro H; cases H; clear H;
+ [1: cases (hos_cotransitive ? h h2 h4 H1); [left;left|right;left] assumption;
+ |2: cases (hos_cotransitive ? h1 h3 h5 H1); [left;right|right;right] assumption;
+ |3: cases (hos_cotransitive ? h2 h h4 H1); [right;left|left;left] assumption;
+ |4: cases (hos_cotransitive ? h3 h1 h5 H1); [right;right|left;right] assumption;]]
+qed.
+
+lemma square_ordered_set: ordered_set → ordered_set.
+intro O; constructor 1;
+[ apply (square_half_ordered_set (os_l O));
+| apply (dual_hos (square_half_ordered_set (os_l O)));
+| reflexivity]
+qed.
+
+notation "s 2 \atop \nleq" non associative with precedence 90
+ for @{ 'square_os $s }.
+notation > "s 'squareO'" non associative with precedence 90
+ for @{ 'squareO $s }.
+interpretation "ordered set square" 'squareO 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).
+