proposition: Lemma topologysubtype_point : ∏ (x : ∑ x : T, dom x) (P : (∑ x0 : T, dom x0) → hProp), topologysubtype x P → P x.
proof: Proof. intros x A. apply hinhuniv. intros B. apply (pr2 (pr2 B)), (pr1 (pr1 (pr2 B))). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Topology.Filters UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.ConstructiveStructures