let t, u, z be Integer; :: thesis: ((t + u) - z) |^ 3,((t |^ 3) + (u |^ 3)) - (z |^ 3) are_congruent_mod 3
(2 * 1) + 1 is odd ;
then A1: (- z) |^ 3 = - (z |^ 3) by POWER:2;
((t + u) + (- z)) |^ 3,((t |^ 3) + (u |^ 3)) + ((- z) |^ 3) are_congruent_mod 3 by LmTUZ;
hence ((t + u) - z) |^ 3,((t |^ 3) + (u |^ 3)) - (z |^ 3) are_congruent_mod 3 by A1; :: thesis: verum