theorem Th10: :: MESFUNC1:10

for r, s being Real st r < s holds
ex n being Element of NAT st 1 / (n + 1) < s - r