for Y being set
for h being PartFunc of REAL,REAL holds
( h | Y is non-decreasing iff for r1, r2 being Real st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds
h . r1 <= h . r2 )