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