theorem Th2: :: SCHEME1:2

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