proposition: Lemma filtergenerated_imply : isfilter_imply filtergenerated.
proof: Proof. intros A B H. apply hinhfun ; intro Ha. exists (pr1 Ha), (pr1 (pr2 Ha)). intros x Hx. apply H. apply (pr2 (pr2 Ha)), Hx. Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.MoreFoundations.PartA