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