for S being non empty non void all-with_const_op ManySortedSign
for U0 being non-empty MSAlgebra over S
for U1, U2 being non-empty MSSubAlgebra of U0 holds the Sorts of U1 (/\) the Sorts of U2 is V8()