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