+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.