theorem Th27: :: FDIFF_12:27

for x0 being Real
for f being PartFunc of REAL,REAL holds
( f is_Lcontinuous_in x0 iff ( x0 in dom f & ( for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x being Real st x in dom f & x0 - d < x & x < x0 holds
|.((f . x) - (f . x0)).| < e ) ) ) ) )