Proofgold Proposition

∀ x0 . x0 ⊆ SNoS_ omega ⟶ ∀ x1 . x1 ⊆ SNoS_ omega ⟶ SNoCutP x0 x1 ⟶ (x0 = 0 ⟶ ∀ x2 : ο . x2) ⟶ (x1 = 0 ⟶ ∀ x2 : ο . x2) ⟶ (∀ x2 . x2 ∈ x0 ⟶ ∃ x3 . and (x3 ∈ x0) (SNoLt x2 x3)) ⟶ (∀ x2 . x2 ∈ x1 ⟶ ∃ x3 . and (x3 ∈ x1) (SNoLt x3 x2)) ⟶ SNoCut x0 x1 ∈ real

type
prop

theory
HotG

name
real_SNoCut_SNoS_omega

proof
PUZ6D..

Megalodon
real_SNoCut_SNoS_omega

proofgold address
TMP6H..^{real_SNoCut_SNoS_omega}

creator
27737 PrQUS../c94a6..

owner
27737 PrQUS../c94a6..

term root
9f139..