proposition: Lemma net_limit_impl_tail_filter_limit: forall x0:point_set X, net_limit x x0 -> filter_limit tail_filter x0.
proof: Proof. intros. red; intros. red; intros U ?. destruct H0. destruct H0 as [V []]. destruct H0. pose proof (H V H0 H2). destruct H3 as [j0]. apply filter_upward_closed with (net_tail j0). - constructor. exists (net_tail j0). split. + exists j0; trivial. constructor. + auto with sets. - intros y ?. apply H1. destruct H4 as [j]. rewrite H5. apply H3. destruct H4; assumption. Qed.
imports: ZornsLemma(Powerset_facts) FilterLimits Nets