theorem :: FDIFF_2:40

for f being PartFunc of REAL,REAL st [#] REAL c= dom f & f is_differentiable_on [#] REAL & ( for x0 being Real holds diff (f,x0) <= 0 ) holds
f | ([#] REAL) is non-increasing