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