Let be a set of formulae in a first-order Language and be a formula in
If then
Proof (NONEXAMINABLE)
By induction on the length of a proof of from
In the case is , there is a subset s.t. doesn’t occur free in , and .
Then by induction
Since does not occur free in , we have and so