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