fact: Definition FilterIntersection {X : UU} (FF : Filter X → hProp) (Hff : ∃ F : Filter X, FF F) : Filter X.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.MoreFoundations.PartA