theorem :: FDIFF_1:10

for Y being Subset of REAL
for f being PartFunc of REAL,REAL st f is_differentiable_on Y holds
Y is open