theorem Th85: :: NEWTON02:183
for a being Nat holds
( not 5 divides (a |^ 2) - 2 & not 5 divides (a |^ 2) + 2 & not 5 divides (a |^ 2) - 3 & not 5 divides (a |^ 2) + 3 )