Proofgold Proposition

∀ x0 x1 . TransSet x0 ⟶ SNo x1 ⟶ SNo x0 ⟶ SNoLev x0 = x0 ⟶ SNoLev x1 = x0 ⟶ not (SNoLe x1 x0) ⟶ not (∀ x2 . ordinal x2 ⟶ x2 ∈ x0 ⟶ x2 ∈ x1)

type
prop

theory
HotG

name
-

proof
PUTNo..

Megalodon
Conj_ordinal_SNoLev_max_2__5__0

proofgold address
TMQX5..^{Conj_ordinal_SNoLev_max_2__5__0}

creator
35053 PrNpY../85e6c..

owner
35061 PrNpY../0623d..

term root
f375f..