proposition: Lemma order_topology_Hausdorff: Hausdorff OrderTopology.
proof: Proof. red. match goal with |- forall x y:point_set OrderTopology, ?P => cut (forall x y:point_set OrderTopology, R x y -> P) end; intros. - destruct (R_total x y). { exact (H x y H1 H0). } assert (y <> x) by auto. destruct (H y x H1 H2) as [V [U [? [? [? []]]]]]. exists U, V. repeat split; trivial. transitivity (Intersection V U); trivial. now extensionality_ensembles. - pose proof (Build_TopologicalSpace_from_subbasis_subbasis _ order_topology_subbasis). destruct (classic (exists z:X, R x z /\ R z y /\ z <> x /\ z <> y)). + destruct H2 as [z [? [? []]]]. exists ([w:X | R w z /\ w <> z]), ([w:X | R z w /\ w <> z]). repeat split; auto. * apply H1. constructor. * apply H1. constructor. * extensionality_ensembles. destruct H6, H7. contradiction H8. now apply (ord_antisym R_ord). + exists ([w:X | R w y /\ w <> y]), ([w:X | R x w /\ w <> x]). repeat split; auto. * apply H1. constructor. * apply H1. constructor. * extensionality_ensembles. destruct H3, H4. contradiction H2. exists x0. now repeat split. Qed.
imports: Subbases SeparatednessAxioms ZornsLemma(EnsemblesTactics)