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