theorem Th3: :: SCHEME1:3

for n being Element of NAT ex m being Element of NAT st
( n = 4 * m or n = (4 * m) + 1 or n = (4 * m) + 2 or n = (4 * m) + 3 )