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