theorem Th4: :: SCHEME1:4

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