proposition: Lemma filter_limit_is_cluster_point: forall {X:TopologicalSpace} (F:Filter X) (x0:point_set X), filter_limit F x0 -> filter_cluster_point F x0.
proof: Proof. intros. red; intros. apply meets_every_open_neighborhood_impl_closure. intros. assert (In (filter_family F) U). { apply H. simpl. constructor. exists U; repeat split; auto with sets. } assert (In (filter_family F) (Intersection S U)). { apply filter_intersection; trivial. } apply NNPP; red; intro. assert (Intersection S U = Empty_set). { apply Extensionality_Ensembles; split; red; intros. - contradiction H5. exists x; trivial. - destruct H6. } rewrite H6 in H4. contradiction (filter_empty _ F). Qed.
imports: ZornsLemma(Powerset_facts)