thus 2 = succ 1
.= (succ 0) \/ {1}
.= (0 \/ {0}) \/ {1}
.= {0,1} by ENUMSET1:1 ; :: thesis: verum