thus 2 = succ 1
.= {0 ,1} by Th87, ENUMSET1:41 ; :: thesis: verum