theorem :: MSUALG_2:36

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S holds Top (MSSubAlLattice U0) = MSAlgebra(# the Sorts of U0, the Charact of U0 #)