theorem Th23: :: RFUNCT_2:23

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