theorem Th28: :: MSSUBLAT:28

for A being Universal_Algebra
for a1, b1 being strict 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)