proposition: Lemma filtertop_notempty : isfilter_notempty filtertop.
proof: Proof. intros A Fa. revert x0. apply hinhfun. intros x0. exists x0. simple refine (Fa _). Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.MoreFoundations.PartA