proposition: Lemma net_cluster_point_impl_tail_filter_cluster_point: forall x0:point_set X, net_cluster_point x x0 -> filter_cluster_point tail_filter x0.
proof: Proof. intros. red; intros. destruct H0. destruct H0 as [T []]. destruct H0 as [j0]. apply meets_every_open_neighborhood_impl_closure. intros. pose proof (H U H3 H4). destruct (H5 j0) as [j' []]. exists (x j'). constructor; trivial. apply H1. rewrite H2. exists j'. - constructor; trivial. - reflexivity. Qed.
imports: ZornsLemma(Powerset_facts) FilterLimits Nets