proposition: Lemma filtertop_imply : isfilter_imply filtertop.
proof: Proof. intros A B H Ha x. apply H. simple refine (Ha _). Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.MoreFoundations.PartA