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