for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for U1 being MSSubAlgebra of U0
for A, B being MSSubset of U0 st B = A (\/) the Sorts of U1 holds
(GenMSAlg A) "\/" U1 = GenMSAlg B