let b be Nat; :: thesis: ( not 3 divides (b |^ 2) + 1 & not 3 divides (b |^ 2) - 2 )
A1: (b |^ 2) + 1 = 3 + ((b |^ 2) - 2) ;
not 3 divides (1 |^ 2) + (b |^ 2) by INT_2:27, Th91;
hence ( not 3 divides (b |^ 2) + 1 & not 3 divides (b |^ 2) - 2 ) by A1, WSIERP_1:4; :: thesis: verum