Proofgold Proposition

∀ x0 . RealsStruct x0 ⟶ RealsStruct_Q x0 = {x2 ∈ field0 x0|∃ x3 . and (x3 ∈ {x5 ∈ field0 x0|or (or (explicit_Field_minus (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0) x5 ∈ RealsStruct_Npos x0) (x5 = field4 x0)) (x5 ∈ RealsStruct_Npos x0)}) (∃ x5 . and (x5 ∈ RealsStruct_Npos x0) (field2b x0 x5 x2 = x3))}

type
prop

theory
HotG

name
-

proof
PUSVY..

Megalodon
-

proofgold address
TMS8k..

creator
5804 Pr6Pc../ecd5b..

owner
5804 Pr6Pc../ecd5b..

term root
61f0c..