Proofgold Proposition

∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ SNoS_ x0 ⟶ SNoLev (minus_SNo x1) ⊆ SNoLev x1

type
prop

theory
HotG

name
minus_SNo_Lev_lem1

proof
PUK1b..

Megalodon
minus_SNo_Lev_lem1

proofgold address
TMcrj..^{minus_SNo_Lev_lem1}

creator
4949 Pr6Pc../433d4..

owner
4949 Pr6Pc../433d4..

term root
14986..