Proofgold Proposition

∀ x0 . ∀ x1 x2 : ι → ο . ∀ x3 . ordinal x0 ⟶ PNoEq_ x0 x1 (λ x4 . or (x1 x4) (x4 = x0)) ⟶ x3 ∈ x0 ⟶ PNoEq_ x3 (λ x4 . or (x1 x4) (x4 = x0)) x2 ⟶ ordinal x3 ⟶ PNoLt x3 x2 x0 x1 ⟶ not (PNoLt x0 x1 x3 x2)

type
prop

theory
HotG

name
-

proof
PUTNo..

Megalodon
Conj_PNo_rel_imv_ex__7__4

proofgold address
TMQfm..^{Conj_PNo_rel_imv_ex__7__4}

creator
35053 PrNpY../6bfa6..

owner
35061 PrNpY../4b5ba..

term root
9eefe..