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