:: deftheorem Def8 defines monotone OSALG_1:def 8 :
for S being OrderSortedSign holds
( S is monotone iff for o being OperSymbol of S holds o is monotone );