:: deftheorem defines monotonic MSAFREE2:def 13 :
for IT being non empty ManySortedSign holds
( IT is monotonic iff for A being non-empty finitely-generated MSAlgebra over IT holds A is finite-yielding );