Theorem 8.2: Any two nonzero natural numbers will have a greatest common factor.
Proof: By Theorem 7.8, a factor of a is less than or equal to a, and a factor of b is less than or equal to b, so the common factors will be contained in the set of numbers which are less than a. By Axiom 1 the common factors will form a set. To see that this set is not empty, note that 1 is a factor of both a and b by Theorem 6.9, the Identity Property of Multiplication. Since the set of common factors is a nonempty set, it has a greatest element by Theorem 5.10, the dual of the Well Ordering Principle.