Proofgold Proposition

∀ x0 . x0 ∈ setexp real omega ⟶ ∀ x1 . x1 ∈ setexp real omega ⟶ (∀ x2 . x2 ∈ omega ⟶ and (and (SNoLe (ap x0 x2) (ap x1 x2)) (SNoLe (ap x0 x2) (ap x0 (add_SNo x2 1)))) (SNoLe (ap x1 (add_SNo x2 1)) (ap x1 x2))) ⟶ ∀ x2 : ο . (∀ x3 . and (x3 ∈ real) (∀ x4 . x4 ∈ omega ⟶ and (SNoLe (ap x0 x4) x3) (SNoLe x3 (ap x1 x4))) ⟶ x2) ⟶ x2

type
prop

theory
HotG

name
real_complete2

proof
PUQV9..

Megalodon
real_complete2

proofgold address
TMKMu..^{real_complete2}

creator
12334 PrGxv../535aa..

owner
12334 PrGxv../535aa..

term root
f33d4..