theorem Th5: :: NUMBER15:5
for m, n being Nat holds
( ( not n mod 4 = 0 & not n mod 4 = 2 ) or (n * m) mod 4 = 0 or (n * m) mod 4 = 2 )