theorem Th31: :: NAT_5:31

for m being Nat
for n0 being non zero Nat st m divides n0 & n0 <> m & m <> 1 holds
(1 + m) + n0 <= sigma n0