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