If ￢∀x∈S (P(x)):
    If ￢∃x∈S (￢P(x)):
        ￢∃y∈S (￢P(y)). // Rename
        Given x∈S:
            If ￢P(x):
                ∃y∈S (￢P(y)). // Exists-Intro since x is unused.
                ￢∃y∈S (￢P(y)). // Restate since y does not occur in it.
            P(x).
        ∀x∈S (P(x)).
        ￢∀x∈S (P(x)). // Restate
        Contradiction.
    ∃x∈S (￢P(x)).
￢∀x∈S (P(x)) → ∃x∈S (￢P(x)).