theorem Th15: :: NAT_6:15

for x being Integer holds
( x |^ 2, 0 are_congruent_mod 3 or x |^ 2,1 are_congruent_mod 3 )