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.