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 (ordsucc x2)))) (SNoLe (ap x1 (ordsucc x2)) (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_complete1

proof
PUQV9..

Megalodon
real_complete1

proofgold address
TMSrg..^{real_complete1}

creator
12334 PrGxv../0f619..

owner
12334 PrGxv../0f619..

term root
05d96..