for S being non empty non void ManySortedSign
for U0, U1 being MSAlgebra over S st MSAlgebra(# the Sorts of U0, the Charact of U0 #) = MSAlgebra(# the Sorts of U1, the Charact of U1 #) holds
U0 is MSSubAlgebra of U1