theorem Th11: :: MESFUNC1:11

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