theorem :: MSSUBLAT:25

for MS being non void 1 -element segmental ManySortedSign
for A being non-empty MSAlgebra over MS st the carrier of MS = {0} holds
the Sorts of A = the Sorts of (MSAlg (1-Alg A))