for S being non empty ManySortedSign st S is trivial holds
for A being MSAlgebra over S
for c1, c2 being Component of the Sorts of A holds c1 = c2