seg_u_ : O
}.
-notation > "đŚ_term 90 s" non associative with precedence 45 for @{'upp $s}.
-notation "đŚ \sub term 90 s" non associative with precedence 45 for @{'upp $s}.
-notation > "đ_term 90 s" non associative with precedence 45 for @{'low $s}.
-notation "đ \sub term 90 s" non associative with precedence 45 for @{'low $s}.
+notation > "đŚ_term 90 s" non associative with precedence 90 for @{'upp $s}.
+notation "đŚ \sub term 90 s" non associative with precedence 90 for @{'upp $s}.
+notation > "đ_term 90 s" non associative with precedence 90 for @{'low $s}.
+notation "đ \sub term 90 s" non associative with precedence 90 for @{'low $s}.
definition seg_u â
ÎťO:half_ordered_set.Îťs:segment O.
cases (wloss_prop O) (E E); do 2 rewrite < E; intros; assumption;
qed.
+lemma l2sl:
+ âC,s.âx,y:half_segment_ordered_set C s. \fst x â¤â¤ \fst y â x â¤â¤ y.
+intros; intro; apply H; apply sx2x; apply H1;
+qed.
+
+
+lemma sl2l:
+ âC,s.âx,y:half_segment_ordered_set C s. x â¤â¤ y â \fst x â¤â¤ \fst y.
+intros; intro; apply H; apply x2sx; apply H1;
+qed.
+
+
lemma h_segment_preserves_supremum:
âO:half_ordered_set.âs:segment O.
âa:sequence (half_segment_ordered_set ? s).