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