let S be non empty non void ManySortedSign ; :: thesis: for U0 being non-empty MSAlgebra over S
for U1, U2 being MSSubAlgebra of U0 holds U1 "\/" U2 = U2 "\/" U1
let U0 be non-empty MSAlgebra over S; :: thesis: for U1, U2 being MSSubAlgebra of U0 holds U1 "\/" U2 = U2 "\/" U1
let U1, U2 be MSSubAlgebra of U0; :: thesis: U1 "\/" U2 = U2 "\/" U1
reconsider u1 = the Sorts of U1, u2 = the Sorts of U2 as MSSubset of U0 by Def9;
( u1 c= the Sorts of U0 & u2 c= the Sorts of U0 ) by PBOOLE:def 18;
then u1 (\/) u2 c= the Sorts of U0 by PBOOLE:16;
then reconsider A = u1 (\/) u2 as MSSubset of U0 by PBOOLE:def 18;
U1 "\/" U2 = GenMSAlg A by Def18;
hence U1 "\/" U2 = U2 "\/" U1 by Def18; :: thesis: verum