let UN be Universe; :: thesis: ( 0 is Element of UN & 1 is Element of UN & 2 is Element of UN )

thus 0 is Element of UN by CLASSES2:56; :: thesis: ( 1 is Element of UN & 2 is Element of UN )

( {} is Element of UN & 1 = succ 0 ) by CLASSES2:56;

hence A1: 1 is Element of UN by Th20; :: thesis: 2 is Element of UN

2 = succ 1 ;

hence 2 is Element of UN by A1, Th20; :: thesis: verum

thus 0 is Element of UN by CLASSES2:56; :: thesis: ( 1 is Element of UN & 2 is Element of UN )

( {} is Element of UN & 1 = succ 0 ) by CLASSES2:56;

hence A1: 1 is Element of UN by Th20; :: thesis: 2 is Element of UN

2 = succ 1 ;

hence 2 is Element of UN by A1, Th20; :: thesis: verum