Proofgold Proposition

∀ x0 . x0 ∈ SNoS_ (ordsucc omega) ⟶ (x0 = omega ⟶ ∀ x1 : ο . x1) ⟶ (x0 = minus_SNo omega ⟶ ∀ x1 : ο . x1) ⟶ (∀ x1 . x1 ∈ SNoS_ omega ⟶ (∀ x2 . x2 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x1 (minus_SNo x0))) (eps_ x2)) ⟶ x1 = x0) ⟶ x0 ∈ real

type
prop

theory
HotG

name
real_I

proof
PUgvb..

Megalodon
real_I

proofgold address
TMXxF..^real_I

creator
12283 PrGxv../c34d1..

owner
12283 PrGxv../c34d1..

term root
b05b9..