theorem Th3: :: LIMFUNC2:3

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