theorem Th4: :: LIMFUNC2:4

for r1, r2 being Real
for f being PartFunc of REAL,REAL st 0 < r2 & ].r1,(r1 + r2).[ c= dom f holds
for r being Real st r1 < r holds
ex g being Real st
( g < r & r1 < g & g in dom f )