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