theorem Th27: :: EC_PF_1:27

for p being Prime
for x being Element of (GF p) st 2 < p & x + x = 0. (GF p) holds
x = 0. (GF p)