for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds
the Sorts of (MSAlg U1) is MSSubset of (MSAlg U2)