Proofgold Proposition

∀ x0 . ordinal x0 ⟶ (∀ x1 . x1 ∈ x0 ⟶ ordsucc x1 ∈ x0) ⟶ ∀ x1 . x1 ⊆ SNoS_ x0 ⟶ ∀ x2 . x2 ⊆ SNoS_ x0 ⟶ SNoCutP x1 x2 ⟶ SNoLev (SNoCut x1 x2) ∈ ordsucc x0

type
prop

theory
HotG

name
SNoCutP_SNoCut_lim

proof
PUgvb..

Megalodon
SNoCutP_SNoCut_lim

proofgold address
TMN8Z..^{SNoCutP_SNoCut_lim}

creator
12283 PrGxv../5fd10..

owner
12283 PrGxv../5fd10..

term root
1a37c..