for A being Universal_Algebra
for a1, b1 being strict non-empty SubAlgebra of A
for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds
the Sorts of a2 (/\) the Sorts of b2 = 0 .--> ( the carrier of a1 /\ the carrier of b1)