theorem Th7: :: MSUALG_2:7

for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra over S st U1 is MSSubAlgebra of U2 & U2 is MSSubAlgebra of U1 holds
MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #)