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