theorem :: MSUALG_2:38
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0 holds the Sorts of U0 in SubSort A by Lm2;