theorem :: LAGRA4SQ:13

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