proposition: Lemma tail_filter_limit_impl_net_limit: forall x0:point_set X, filter_limit tail_filter x0 -> net_limit x x0.
proof: Proof. intros. intros U ? ?. assert (In (filter_family tail_filter) U). { apply H. constructor. apply open_neighborhood_is_neighborhood. split; trivial. } destruct H2. destruct H2 as [T []]. destruct H2 as [j0]. exists j0. intros. apply H3. rewrite H4. exists j; trivial. constructor; assumption. Qed.
imports: ZornsLemma(Powerset_facts) FilterLimits Nets