for U1 being Universal_Algebra holds MSAlg (id the carrier of U1) = id the Sorts of (MSAlg U1)