theorem Th41: :: FDIFF_2:41

for g, p being Real
for f being PartFunc of REAL,REAL st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x0 being Real st x0 in ].p,g.[ holds
0 < diff (f,x0) or for x0 being Real st x0 in ].p,g.[ holds
diff (f,x0) < 0 ) holds
rng (f | ].p,g.[) is open