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