theorem Th9: :: MESFUNC1:9

for r being Real ex n being Nat st - n <= r