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