proposition: Lemma net_limit_is_unique_cluster_point_impl_Hausdorff: forall (X:TopologicalSpace), (forall (I:DirectedSet) (x:Net I X) (x0 y:point_set X), net_limit x x0 -> net_cluster_point x y -> y = x0) -> Hausdorff X.
proof: Proof. intros. red; intros. assert (~ net_cluster_point (neighborhood_net _ x) y). { intro. contradiction H0. symmetry. apply H with _ (neighborhood_net _ x); trivial. apply neighborhood_net_limit. } apply not_all_ex_not in H1. destruct H1 as [V]. apply imply_to_and in H1. destruct H1. apply imply_to_and in H2. destruct H2. apply not_all_ex_not in H3. destruct H3 as [[U]]. exists U, V. repeat split; trivial. extensionality_ensembles. contradiction H3. exists (intro_neighborhood_net_DS X x U x0 o i H4). split; trivial. simpl. auto with sets. Qed.
imports: Coq(Program.Subset) Topology(Homeomorphisms SubspaceTopology)