:: deftheorem Def3 defines trivial MSAFREE4:def 3 :
for S being non empty non void ManySortedSign
for A being MSAlgebra over S holds
( A is trivial iff the Sorts of A is V275() );