proposition: Lemma Hausdorff_impl_net_limit_unique: forall {X:TopologicalSpace} {I:DirectedSet} (x:Net I X), Hausdorff X -> uniqueness (net_limit x).
proof: Proof. intros. red; intros x1 x2 ? ?. apply NNPP. intro. destruct (H x1 x2) as [U [V [? [? [? [? ?]]]]]]; trivial. destruct (H0 U H3 H5) as [i]. destruct (H1 V H4 H6) as [j]. destruct (DS_join_cond i j) as [k [? ?]]. assert (In (Intersection U V) (x k)). { constructor. - now apply H8. - now apply H9. } rewrite H7 in H12. destruct H12. Qed.
imports: Coq(Program.Subset) Topology(Homeomorphisms SubspaceTopology)