proposition: Lemma filter_cluster_point_impl_filter_to_net_cluster_point: forall x0:point_set X, filter_cluster_point F x0 -> net_cluster_point filter_to_net x0.
proof: Proof. intros. red; intros. red; intros. destruct i. pose proof (H ftn_S0 ftn_S_in_F0). pose proof (closure_impl_meets_every_open_neighborhood _ _ _ H2 U H0 H1). destruct H3. destruct H3. exists (Build_filter_to_net_DS_set ftn_S0 x ftn_S_in_F0 H3). simpl. split; auto with sets. Qed.
imports: ZornsLemma(Powerset_facts) FilterLimits Nets