thus 10 = succ 9
.= {0,1,2,3,4,5,6,7,8,9} by Th55, ENUMSET1:85 ; :: thesis: verum