theorem Th27: :: MSUALG_2:27

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for U1, U2 being MSSubAlgebra of U0 holds U1 /\ (U1 "\/" U2) = MSAlgebra(# the Sorts of U1, the Charact of U1 #)