proposition: Lemma ultrafilter_cluster_point_is_limit: forall {X:TopologicalSpace} (F:Filter X) (x0:point_set X), filter_cluster_point F x0 -> ultrafilter F -> filter_limit F x0.
proof: Proof. intros. red. red; intros N ?. destruct H1. destruct H1 as [U [[]]]. cut (In (filter_family F) U). { intros; apply filter_upward_closed with U; trivial. } clear N H3. apply NNPP; intro. assert (In (filter_family F) (Complement U)). { pose proof (H0 U). tauto. } pose proof (H _ H4). rewrite closure_fixes_closed in H5. - contradiction H5; trivial. - red; rewrite Complement_Complement; trivial. Qed.
imports: ZornsLemma(Powerset_facts)