proposition: Lemma filtertop_and : isfilter_and filtertop.
proof: Proof. intros A B Ha Hb x. split. + simple refine (Ha _). + simple refine (Hb _). Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.MoreFoundations.PartA