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