theorem :: NUMBER06:2
for p being even Prime holds p = 2 by INT_2:def 4, ABIAN:def 1;