:: deftheorem defines monotone RFUNCT_2:def 5 :
for h being PartFunc of REAL,REAL holds
( h is monotone iff ( h is non-decreasing or h is non-increasing ) );