theorem Th28: :: NUMBER02:28

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