let a, b be Nat; :: thesis: ( 3 divides ((a + b) * (a - b)) + (a * b) iff ( 3 divides a & 3 divides b ) )
( 3 divides a & 3 divides b implies 3 divides a + b ) by WSIERP_1:4;
hence ( 3 divides ((a + b) * (a - b)) + (a * b) iff ( 3 divides a & 3 divides b ) ) by Lm33, Lm34, WSIERP_1:5; :: thesis: verum