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