proposition: Lemma PreFilterTop_correct {X : UU} : ∏ (F : PreFilter X), filter_le F PreFilterTop.
proof: Proof. intros F A Ha. apply filter_forall, Ha. Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.MoreFoundations.PartA