theorem :: FDIFF_12:26

for f being PartFunc of REAL,REAL
for x0 being Real st x0 in dom f & f is_continuous_in x0 holds
( f is_Lcontinuous_in x0 & f is_Rcontinuous_in x0 )