proposition: Lemma filter_to_net_limit_impl_filter_limit: forall x0:point_set X, net_limit filter_to_net x0 -> filter_limit F x0.
proof: Proof. intros. intros U ?. destruct H0. destruct H0 as [V []]. apply filter_upward_closed with V; trivial. destruct H0. destruct (H V H0 H2) as [[]]. apply filter_upward_closed with ftn_S0. { trivial. } red; intros. pose proof (H3 (Build_filter_to_net_DS_set ftn_S0 x ftn_S_in_F0 H4)). simpl in H5. apply H5; auto with sets. Qed.
imports: ZornsLemma(Powerset_facts) FilterLimits Nets