let n, k, l be Nat; :: thesis: ( 3 divides n + l iff 3 divides (n + l) + (3 * k) )

hereby :: thesis: ( 3 divides (n + l) + (3 * k) implies 3 divides n + l )

assume A1: 3 divides n + l ; :: thesis: 3 divides (n + l) + (3 * k)
3 divides 3 * k ;
hence 3 divides (n + l) + (3 * k) by A1, WSIERP_1:4; :: thesis: verum

end;

assume A1: 3 divides (n + l) + (3 * k) ; :: thesis: 3 divides n + l
3 divides 3 * k ;
then 3 divides ((n + l) + (3 * k)) - (3 * k) by A1, PREPOWER:94;
hence 3 divides n + l ; :: thesis: verum