Proofgold Proposition

∀ x0 . RealsStruct x0 ⟶ ∀ x1 : ο . (RealsStruct_Q x0 ⊆ field0 x0 ⟶ (∀ x2 . x2 ∈ RealsStruct_Q x0 ⟶ ∀ x3 : ο . (x2 ∈ field0 x0 ⟶ ∀ x4 . x4 ∈ RealsStruct_Z x0 ⟶ ∀ x5 . x5 ∈ RealsStruct_Npos x0 ⟶ field2b x0 x5 x2 = x4 ⟶ x3) ⟶ x3) ⟶ (∀ x2 . x2 ∈ field0 x0 ⟶ ∀ x3 . x3 ∈ RealsStruct_Z x0 ⟶ ∀ x4 . x4 ∈ RealsStruct_Npos x0 ⟶ field2b x0 x4 x2 = x3 ⟶ x2 ∈ RealsStruct_Q x0) ⟶ x1) ⟶ x1

type
prop

theory
HotG

name
RealsStruct_Q_props

proof
PUSVY..

Megalodon
RealsStruct_Q_props

proofgold address
TMFXP..^{RealsStruct_Q_props}

creator
5804 Pr6Pc../ec06d..

owner
5804 Pr6Pc../ec06d..

term root
df790..