Proofgold Proposition

∀ x0 . ordinal x0 ⟶ SNoLt 0 (ordsucc x0)

type
prop

theory
HotG

name
ordinal_ordsucc_pos

proof
PUVXT..

Megalodon
ordinal_ordsucc_pos

proofgold address
TMXAm..^{ordinal_ordsucc_pos}

creator
29757 PrQUS../82eff..

owner
29757 PrQUS../82eff..

term root
9af5d..