theorem Th20: :: RFUNCT_2:20

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