theorem Th92: :: NUMBER14:92
for a, b, c being Integer holds
( (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 0 or (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 1 or (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 2 or (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 3 or (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 4 or (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 5 or (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 6 )