for a being Element of NAT
for p being Prime st p |^ 2 divides a holds
p divides a