theorem Th24: :: NUMBER02:24

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