theorem :: RFUNCT_2:43

for x being set
for h being PartFunc of REAL,REAL holds h | {x} is non-increasing