theorem Th8: :: FDIFF_1:8
for X being set
for f being PartFunc of REAL,REAL st f is_differentiable_on X holds
X is Subset of REAL by XBOOLE_1:1;