let n be Nat; :: thesis: for a, b, c being Prime holds
( not (n |^ 2) - 1 = (a * b) * c or n - 1 is prime or n + 1 is prime )
let a, b, c be Prime; :: thesis: ( not (n |^ 2) - 1 = (a * b) * c or n - 1 is prime or n + 1 is prime )
assume A1: (n |^ 2) - 1 = (a * b) * c ; :: thesis: ( n - 1 is prime or n + 1 is prime )
A2: n |^ 2 = n ^2 by WSIERP_1:1;
then A3: (n |^ 2) - 1 = (n - 1) * (n + 1) ;

A4: now :: thesis: not n < 1

assume n < 1 ; :: thesis: contradiction
then n = 0 by NAT_1:14;
hence contradiction by A1; :: thesis: verum

end;

c divides (n - 1) * (n + 1) by A1, A2;

per cases then ( c divides n - 1 or c divides n + 1 ) by INT_5:7;

suppose c divides n - 1 ; :: thesis: ( n - 1 is prime or n + 1 is prime )

then c * (n + 1) divides (n - 1) * (n + 1) by NAT_3:1;
then ( n + 1 = 0 + 1 or n + 1 = a or n + 1 = b or n + 1 = a * b ) by A1, A2, GROUP_22:1, GR_CY_3:1;

per cases then ( n + 1 = a or n + 1 = b or n + 1 = a * b ) by A1;

suppose ( n + 1 = a or n + 1 = b ) ; :: thesis: ( n - 1 is prime or n + 1 is prime )

hence ( n - 1 is prime or n + 1 is prime ) ; :: thesis: verum

end;

suppose n + 1 = a * b ; :: thesis: ( n - 1 is prime or n + 1 is prime )

hence ( n - 1 is prime or n + 1 is prime ) by A1, A3, XCMPLX_1:5; :: thesis: verum

end;

end;

end;

suppose c divides n + 1 ; :: thesis: ( n - 1 is prime or n + 1 is prime )

then c * (n - 1) divides (n + 1) * (n - 1) by NAT_3:1;

per cases then ( n - 1 = 1 or n - 1 = a or n - 1 = b or n - 1 = a * b ) by A1, A2, A4, GROUP_22:1, GR_CY_3:1;

suppose n - 1 = 1 ; :: thesis: ( n - 1 is prime or n + 1 is prime )

hence ( n - 1 is prime or n + 1 is prime ) by XPRIMES1:3; :: thesis: verum

end;

suppose ( n - 1 = a or n - 1 = b ) ; :: thesis: ( n - 1 is prime or n + 1 is prime )

hence ( n - 1 is prime or n + 1 is prime ) ; :: thesis: verum

end;

suppose n - 1 = a * b ; :: thesis: ( n - 1 is prime or n + 1 is prime )

hence ( n - 1 is prime or n + 1 is prime ) by A1, A3, XCMPLX_1:5; :: thesis: verum

end;

end;

end;

end;