theorem Th11: :: INTEGR26:11

for a, b, x being Real
for f being PartFunc of REAL,REAL st [.a,b.] c= dom f & f | [.a,b.] is continuous & x in ].a,b.] holds
( f is_left_convergent_in x & lim_left ((f | ].a,b.[),x) = f . x )