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