theorem Th21: :: RFUNCT_2:21

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