let S be non empty non void ManySortedSign ; :: thesis: for U0 being MSAlgebra of S
for U1, U2 being strict MSSubAlgebra of U0 st the Sorts of U1 = the Sorts of U2 holds
U1 = U2
let U0 be MSAlgebra of S; :: thesis: for U1, U2 being strict MSSubAlgebra of U0 st the Sorts of U1 = the Sorts of U2 holds
U1 = U2
let U1, U2 be strict MSSubAlgebra of U0; :: thesis: ( the Sorts of U1 = the Sorts of U2 implies U1 = U2 )
assume the Sorts of U1 = the Sorts of U2 ; :: thesis: U1 = U2
then ( U1 is strict MSSubAlgebra of U2 & U2 is strict MSSubAlgebra of U1 ) by Th9;
hence U1 = U2 by Th8; :: thesis: verum