fact: Record filter_to_net_DS_set : Type := { ftn_S : Ensemble (point_set X); ftn_x : point_set X; ftn_S_in_F : In (filter_family F) ftn_S; ftn_x_in_S : In ftn_S ftn_x }.
imports: ZornsLemma(Powerset_facts) FilterLimits Nets