| ∀ x0 . equip 3 x0 ⟶ ∀ x1 : ο . (∀ x2 . and (x2 ∈ x0) (∀ x3 : ο . (∀ x4 . and (x4 ∈ x0) (∀ x5 : ο . (∀ x6 . and (x6 ∈ x0) (and (and (and (x2 = x4 ⟶ ∀ x7 : ο . x7) (x2 = x6 ⟶ ∀ x7 : ο . x7)) (x4 = x6 ⟶ ∀ x7 : ο . x7)) (∀ x7 . x7 ∈ x0 ⟶ or (or (x7 = x2) (x7 = x4)) (x7 = x6))) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1 |
|