Proofgold Proposition

∀ x0 . x0 ∈ SNoS_ omega ⟶ SNoLe 0 x0 ⟶ sqrt_SNo_nonneg x0 ∈ real

type
prop

theory
HotG

name
sqrt_SNo_nonneg_SNoS_omega

proof
PUTdS..

Megalodon
sqrt_SNo_nonneg_SNoS_omega

proofgold address
TMWqk..^{sqrt_SNo_nonneg_SNoS_omega}

creator
27893 PrQUS../f385e..

owner
27893 PrQUS../f385e..

term root
6aa09..