#### Supplement to Frege's Theorem and Foundations for Arithmetic

## A More Complex Example

If given the premise that

1+2^{2}=5

one can prove that

1 ∈ ε[λzz+2^{2}=5]

For it follows from our premise (by λ-Abstraction) that:

[λzz+2^{2}=5]1

Independently, by the logic of identity, we know:

ε[λzz+2^{2}=5] = ε[λzz+2^{2}=5]

So we may conjoin this fact and the result of λ-Abstraction to produce:

ε[λzz+2^{2}=5] = ε[λzz+2^{2}=5] & [λzz+2^{2}=5]1

Then, by existential generalization on the concept
[λ*z* *z*+2^{2}=5], it follows that:

∃G[ε[λzz+2^{2}=5] = εG&G1]

And, finally, By the definition of membership, we obtain:

1 ∈ ε[λzz+2^{2}=5],

which is what we were trying to prove.