theorem Th32: :: NUMBER02:32

for n being Nat holds
( not 4 divides n iff ex k being Nat st
( n = (4 * k) + 1 or n = (4 * k) + 2 or n = (4 * k) + 3 ) )