let a, b be Nat; :: thesis: ( 3 divides a * b or 3 divides a + b or 3 divides a - b )

per cases ( 3 divides a or 3 divides b or ( not 3 divides a & not 3 divides b ) ) ;

suppose ( 3 divides a or 3 divides b ) ; :: thesis: ( 3 divides a * b or 3 divides a + b or 3 divides a - b )

hence ( 3 divides a * b or 3 divides a + b or 3 divides a - b ) by INT_2:2; :: thesis: verum

end;

suppose ( not 3 divides a & not 3 divides b ) ; :: thesis: ( 3 divides a * b or 3 divides a + b or 3 divides a - b )

per cases then ( ( 3 divides a + 1 & 3 divides b + 1 ) or ( 3 divides a - 1 & 3 divides b - 1 ) or ( 3 divides a - 1 & 3 divides b + 1 ) or ( 3 divides a + 1 & 3 divides b - 1 ) ) by Th90;

suppose ( 3 divides a + 1 & 3 divides b + 1 ) ; :: thesis: ( 3 divides a * b or 3 divides a + b or 3 divides a - b )

then 3 divides (a + 1) - (b + 1) by INT_5:1;
hence ( 3 divides a * b or 3 divides a + b or 3 divides a - b ) ; :: thesis: verum

end;

suppose ( 3 divides a - 1 & 3 divides b - 1 ) ; :: thesis: ( 3 divides a * b or 3 divides a + b or 3 divides a - b )

then 3 divides (a - 1) - (b - 1) by INT_5:1;
hence ( 3 divides a * b or 3 divides a + b or 3 divides a - b ) ; :: thesis: verum

end;

suppose ( 3 divides a - 1 & 3 divides b + 1 ) ; :: thesis: ( 3 divides a * b or 3 divides a + b or 3 divides a - b )

then 3 divides (a - 1) + (b + 1) by WSIERP_1:4;
hence ( 3 divides a * b or 3 divides a + b or 3 divides a - b ) ; :: thesis: verum

end;

suppose ( 3 divides a + 1 & 3 divides b - 1 ) ; :: thesis: ( 3 divides a * b or 3 divides a + b or 3 divides a - b )

then 3 divides (a + 1) + (b - 1) by WSIERP_1:4;
hence ( 3 divides a * b or 3 divides a + b or 3 divides a - b ) ; :: thesis: verum

end;

end;

end;

end;