Proofgold Proposition

∀ x0 x1 . TransSet x0 ⟶ (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ SNoS_ x2 ⟶ SNoLev (minus_SNo x3) ⊆ SNoLev x3) ⟶ ordinal (SNoLev x1) ⟶ SNo x1 ⟶ SNoCutP (prim5 (SNoR x1) minus_SNo) (prim5 (SNoL x1) minus_SNo) ⟶ SNoLev (minus_SNo x1) ⊆ SNoLev x1

type
prop

theory
HotG

name
-

proof
PURzn..

Megalodon
Conj_minus_SNo_Lev_lem1__22__2

proofgold address
TMU48..^{Conj_minus_SNo_Lev_lem1__22__2}

creator
35045 PrNpY../efeab..

owner
35047 PrNpY../283d3..

term root
7239d..