theorem Th3: :: FCONT_1:3

for x0 being Real
for f being PartFunc of REAL,REAL holds
( f is_continuous_in x0 iff for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds
|.((f . x1) - (f . x0)).| < r ) ) )