λ x0 x1 . ∀ x2 . x2 ∈ x1 ⟶ ∀ x3 : ο . (∀ x4 . and (SNo x4) (or (x2 ∈ x4) (∀ x5 : ο . (∀ x6 . and (x6 ∈ x4) (∀ x7 : ο . (∀ x8 . and (x8 ∈ x0) (and (1 ∈ x8) (x2 = SetAdjoin x6 (Sing x8))) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5)) ⟶ x3) ⟶ x3 |
|