If ∃x ∈ S (x ∈ S):
    ∀y ∈ S P(y) ∨ ￢∀y ∈ S P(y)

    If ∀y ∈ S P(y):
        P(c)
        If P(c):
            ∀y ∈ S P(y)
        P(c) → ∀y ∈ S P(y)

    If ￢∀y ∈ S P(y):
        ∃y ∈ S ￢P(y)
        Let c be a constant such that ￢P(c)
        ￢P(c)
        If P(c):
            ⊥
            ∀y ∈ S P(y)
        P(c) → ∀y ∈ S P(y)

    P(c) → ∀y ∈ S P(y)
    ∃x ∈ S (P(x) → ∀y ∈ S P(y))

∃x ∈ S (x ∈ S) → ∃x ∈ S (P(x) → ∀y ∈ S P(y))