theorem Th51: :: NUMBER08:51
for n being Nat
for a, b, c being Prime holds
( not (n |^ 2) - 1 = (a * b) * c or n - 1 is prime or n + 1 is prime )