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