theorem Th13: :: INTEGR26:13

for x being Real
for f being PartFunc of REAL,REAL
for I being non empty Interval
for X being Subset of REAL st I c= X & x in I & x <> inf I holds
( f is_left_differentiable_in x iff f | X is_left_differentiable_in x )