Proofgold Proposition

∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ exactly1of3 (x0 ∈ x1) (x0 = x1) (x1 ∈ x0)

type
prop

theory
HotG

name
ordinal_trichotomy

proof
PUMB7..

Megalodon
ordinal_trichotomy

proofgold address
TMadv..^{ordinal_trichotomy}

creator
4898 Pr6Pc../5d5ec..

owner
4898 Pr6Pc../5d5ec..

term root
2230c..