:: deftheorem Def12 defines Trivial_Algebra MSAFREE2:def 12 :
for S being non empty ManySortedSign
for b₂ being strict MSAlgebra over S holds
( b₂ = Trivial_Algebra S iff the Sorts of b₂ = the carrier of S --> {0} );