theorem DivisorsSquare: :: LATSTONE:27

for p being Prime holds NatDivisors (p * p) = {1,p,(p * p)}