## Theorem 5.8: Every Element of a Von Neumann Integer is also a Subset of that Integer

#### This example shows a file containing a number of theorems, some
of which
are proved. The proofs given are all checkable. The proof
whose check output is shown is theorem 5.8.

####

This example comes from Kelley-Morse set theory.
In this set theory the set of x satisfying any condition
whatsoever always exists. Membership however depends on
membership in the universe as well as satisfaction of the
defining condition. This example pertains to the Von Neumann integers,
commonly represented by the
letter omega, ω.
In the Von Neumann model of the integers, zero is represented by
the empty set. The number 1 = {0}.
The number 2 = {0,1}, and so on. In general
every natural number is equal to the set of the preceding natural
numbers. scsr x is the union of x with {x}, the successor of x in other words.

Theorem 5.8 says that
every element y of a natural number x is a subset of x.

Note 1 begins the proof by defining the set A of all x with the property
that each element y of x is also a subset of x.
The theorem asserts that ω is a subset of A.
The proof is an induction proof that ω is a subset of A.

Note 2 unwraps note 1 yielding the condition that x belongs to
A if and only if x belongs to the universe and every
element y of x is a subset of x.

This proof is an induction proof. Note 3 is the base case and the induction
step is completed in Note 9.
The induction step begins in Note 4 which takes the assumption that x belongs to A as
a given.

Notes 5 and 6 use Note 2 to state what is known about x.
In Note 7 it is shown that every element of the successor of x is a subset
of the successor of x.

But in Note 8 we see that this means that the successor of x is an element of A.
The proof of Note 8 uses Note 7 and Theorem 4.3 which states that if x is in the universe
then so is the successor of x.

Note 9 closes the given-hence block opened in Note 4. (Note 4 can only be used
as a given inside this block.)

Note 10 is proved by appealing to the Theorem 5.7,
the induction theorem for Von Nemann integers, Note 3 the base case of the
induction and Note 9 (Universalized) which is the induction step.
Another note is required because the theorem must be proved just
as it was stated.