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