Description: Lemma for fin1a2 . The successor operation on the ordinal numbers is injective or one-to-one. Lemma 1.17 of Schloeder p. 2. (Contributed by Stefan O'Rear, 7-Nov-2014)