theorem Th13: :: PDIFF_9:13

for m, n being non zero Element of NAT
for X being Subset of (REAL m)
for f being PartFunc of (REAL m),(REAL n) st f is_differentiable_on X holds
X is open by PDIFF_6:33;