theorem Th8: :: MESFUNC1:8

for r being Real ex n being Element of NAT st r <= n