thus 5 = succ 4
.= {0 ,1,2,3,4} by Th90, ENUMSET1:50 ; :: thesis: verum