Proofgold Proposition

∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ordsucc x1 ⊆ x0

type
prop

theory
HotG

name
ordinal_ordsucc_In_Subq

proof
PUL8Q..

Megalodon
ordinal_ordsucc_In_Subq

proofgold address
TMaxm..^{ordinal_ordsucc_In_Subq}

creator
4882 Pr6Pc../cb54b..

owner
4882 Pr6Pc../cb54b..

term root
57345..