proposition: Lemma contained_in_union_open (U : A) : pr1 U ⊆ ⋃ A.
proof: Proof. intros x Hx. apply hinhpr. exists (pr1 U). use make_dirprod. - apply hinhpr. exists (pr21 U). exact (pr2 U). - exact Hx. Qed.
imports: UniMath.MoreFoundations.Subtypes UniMath.Topology.Topology