:: deftheorem Def2 defines decreasing RFUNCT_2:def 2 :
for h being PartFunc of REAL,REAL holds
( h is decreasing iff for r1, r2 being Real st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r2 < h . r1 );