fact: Definition isPreFilter {X : UU} (F : (X → hProp) → hProp) := isfilter_imply F × isfilter_finite_intersection F.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.MoreFoundations.PartA