proposition: Lemma filter_limit_impl_filter_to_net_limit: forall x0:point_set X, filter_limit F x0 -> net_limit filter_to_net x0.
proof: Proof. intros. intros U ? ?. assert (In (filter_family F) U). { apply H. constructor. apply open_neighborhood_is_neighborhood. split; trivial. } exists (Build_filter_to_net_DS_set U x0 H2 H1). destruct j. simpl. auto. Qed.
imports: ZornsLemma(Powerset_facts) FilterLimits Nets