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