proposition: Lemma topologyfromneighborhood_open : isSetOfOpen_union (λ A : X → hProp, make_hProp (topologyfromneighborhood A) (isaprop_topologyfromneighborhood A)).
proof: Proof. intros L Hl x. apply hinhuniv. intros A. apply Himpl with (pr1 A). - intros y Hy. apply hinhpr. now exists (pr1 A), (pr1 (pr2 A)). - apply Hl. + exact (pr1 (pr2 A)). + exact (pr2 (pr2 A)). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Topology.Filters UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.ConstructiveStructures