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