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