theorem Th3: :: SEQ_4:3

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