:: deftheorem defines times-monotone QUANTAL1:def 14 :
for Q being non empty QuantaleStr
for IT being UnOp of Q holds
( IT is times-monotone iff for a, b being Element of Q holds (IT . a) [*] (IT . b) [= IT . (a [*] b) );