proposition: Lemma isSetOfOpen_hfalse : isSetOfOpen_union → O (λ _ : X, hfalse).
proof: Proof. intros H0. rewrite <- union_hfalse. apply H0. intro. apply fromempty. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Topology.Filters UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.ConstructiveStructures