for U1, U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of MSAlg U2 holds
the carrier of U1 is Subset of U2