proposition: Lemma FilterTop_correct {X : UU} : ∏ (x0 : ∥ X ∥) (F : Filter X), filter_le F (FilterTop x0).
proof: Proof. intros x0 F A Ha. apply PreFilterTop_correct, Ha. Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.MoreFoundations.PartA