-
-definition segment ≝ λO:ordered_set.λa,b:O.λx:O.
- (cic:/matita/logic/connectives/And.ind#xpointer(1/1) (x ≤ b) (a ≤ x)).
-
-notation "[a,b]" non associative with precedence 50
- for @{'segment $a $b}.
-interpretation "Ordered set sergment" 'segment a b = (segment _ a b).
-
-notation "hvbox(x \in break [a,b])" non associative with precedence 50
- for @{'segment2 $a $b $x}.
-interpretation "Ordered set sergment in" 'segment2 a b x= (segment _ a b x).
-
-coinductive sigma (A:Type) (P:A→Prop) : Type ≝ sig_in : ∀x.P x → sigma A P.
-
-definition pi1 : ∀A.∀P.sigma A P → A ≝ λA,P,s.match s with [sig_in x _ ⇒ x].
-
-interpretation "sigma pi1" 'pi1 x = (pi1 _ _ x).
-
-interpretation "Type exists" 'exists \eta.x =
- (cic:/matita/dama/supremum/sigma.ind#xpointer(1/1) _ x).
+definition segment ≝ λO:half_ordered_set.λa,b:O.λx:O.(x ≤≤ b) ∧ (a ≤≤ x).
+
+notation "[term 19 a,term 19 b]" non associative with precedence 90 for @{'segment $a $b}.
+interpretation "Ordered set sergment" 'segment a b = (segment (os_l _) a b).
+
+notation "hvbox(x \in break [term 19 a, term 19 b])" non associative with precedence 45
+ for @{'segment_in $a $b $x}.
+interpretation "Ordered set sergment in" 'segment_in a b x= (segment (os_l _) a b x).
+
+definition segment_ordered_set_carr ≝
+ λO:half_ordered_set.λu,v:O.∃x.segment ? u v x.
+definition segment_ordered_set_exc ≝
+ λO:half_ordered_set.λu,v:O.
+ λx,y:segment_ordered_set_carr ? u v.\fst x ≰≰ \fst y.
+lemma segment_ordered_set_corefl:
+ ∀O,u,v. coreflexive ? (segment_ordered_set_exc O u v).
+intros 4; cases x; simplify; apply hos_coreflexive; qed.
+lemma segment_ordered_set_cotrans :
+ ∀O,u,v. cotransitive ? (segment_ordered_set_exc O u v).
+intros 6 (O u v x y z); cases x; cases y ; cases z; simplify; apply hos_cotransitive;
+qed.
+
+lemma half_segment_ordered_set:
+ ∀O:half_ordered_set.∀u,v:O.half_ordered_set.
+intros (O u v); apply (mk_half_ordered_set ?? (segment_ordered_set_corefl O u v) (segment_ordered_set_cotrans ???));
+qed.