let t, u, z be Integer; :: thesis: ( not u + t = z or 3 divides (u * t) * z or 3 divides u - t )
assume u + t = z ; :: thesis: ( 3 divides (u * t) * z or 3 divides u - t )
then 3 divides ((u + t) - z) + (3 * z) ;
then 3 divides (u + t) + (2 * z) ;
then ( 3 divides (u * t) * (2 * z) or u mod 3 = t mod 3 ) by LmABC;
then ( 3 divides 2 * ((u * t) * z) or u,t are_congruent_mod 3 ) by NAT_D:64;
hence ( 3 divides (u * t) * z or 3 divides u - t ) by PEPIN:41, INT_2:25, INT_2:28, INT_2:30; :: thesis: verum