Proofgold Proposition

∀ x0 x1 x2 . x0 ⊆ Sep real (SNoLe 0) ⟶ x1 ⊆ Sep real (SNoLe 0) ⟶ x2 ∈ real ⟶ SNoLe 0 x2 ⟶ SNo_sqrtauxset x0 x1 x2 ⊆ Sep real (SNoLe 0)

type
prop

theory
HotG

name
SNo_sqrtauxset_real_nonneg

proof
PUTdS..

Megalodon
SNo_sqrtauxset_real_nonneg

proofgold address
TMbkh..^{SNo_sqrtauxset_real_nonneg}

creator
27893 PrQUS../1576b..

owner
27893 PrQUS../1576b..

term root
1c421..