thus 4 = succ 3
.= {0 ,1,2,3} by Th89, ENUMSET1:46 ; :: thesis: verum