:: deftheorem defines monotone OSALG_1:def 21 :
for S being OrderSortedSign
for A being OSAlgebra of S holds
( A is monotone iff for o1, o2 being OperSymbol of S st o1 <= o2 holds
(Den (o2,A)) | (Args (o1,A)) = Den (o1,A) );