proposition: Lemma filter_to_net_cluster_point_impl_filter_cluster_point: forall x0:point_set X, net_cluster_point filter_to_net x0 -> filter_cluster_point F x0.
proof: Proof. intros. red; intros. apply meets_every_open_neighborhood_impl_closure; intros. assert (Inhabited S). { apply NNPP; red; intro. pose proof (not_inhabited_empty S H3). subst. contradiction (filter_empty _ F). } destruct H3 as [y]. pose (j0 := Build_filter_to_net_DS_set S y H0 H3). destruct (H U H1 H2 j0) as [j' []]. exists (filter_to_net j'). constructor; trivial. destruct j'. simpl. simpl in H5. simpl in H4. auto. Qed.
imports: ZornsLemma(Powerset_facts) FilterLimits Nets