proposition: Lemma filterintersection_notempty : isfilter_notempty filterintersection.
proof: Proof. intros A Fa. revert His. apply hinhuniv. intros F. apply (Hempty (pr1 F)). * exact (pr2 F). * simple refine (Fa _ _). exact (pr2 F). Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.MoreFoundations.PartA