proposition: Lemma tail_filter_cluster_point_impl_net_cluster_point: forall x0:point_set X, filter_cluster_point tail_filter x0 -> net_cluster_point x x0.
proof: Proof. intros. red; intros. red; intros. assert (In (closure (net_tail i)) x0). { apply H. constructor. exists (net_tail i). split. - exists i; trivial. constructor. - auto with sets. } pose proof (closure_impl_meets_every_open_neighborhood _ _ _ H2 U H0 H1). destruct H3. destruct H3. destruct H3. exists x1; split. - destruct H3; trivial. - rewrite <- H5; trivial. Qed.
imports: ZornsLemma(Powerset_facts) FilterLimits Nets