Proofgold Proposition

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

type
prop

theory
HotG

name
TransSet_ordsucc_In_Subq

proof
PUL8Q..

Megalodon
TransSet_ordsucc_In_Subq

proofgold address
TMTRB..^{TransSet_ordsucc_In_Subq}

creator
4882 Pr6Pc../0cad4..

owner
4882 Pr6Pc../0cad4..

term root
d5d88..