proposition: Lemma lower_closed_interval_closed: forall x:X, closed [ y:X | R y x ] (X:=OrderTopology).
proof: Proof. intro. red. match goal with |- open ?U => replace U with (interior U) end. { apply interior_open. } apply Extensionality_Ensembles; split. { apply interior_deflationary. } intros y ?. red in H. red in H. assert (R x y). { destruct (R_total x y); trivial. now contradiction H. } exists [z:X | R x z /\ z <> x]; constructor; split; trivial. - apply (Build_TopologicalSpace_from_subbasis_subbasis _ order_topology_subbasis). constructor. - red. intros z ?. destruct H1. destruct H1. intro. destruct H3. contradiction H2. now apply (ord_antisym R_ord). - intro. contradiction H. constructor. now subst. Qed.
imports: Subbases SeparatednessAxioms ZornsLemma(EnsemblesTactics)