let S be non empty non void ManySortedSign ; :: thesis: for U0 being non-empty MSAlgebra of S holds MSAlg_join U0 is commutative
let U0 be non-empty MSAlgebra of S; :: thesis: MSAlg_join U0 is commutative
set o = MSAlg_join U0;
for x, y being Element of MSSub U0 holds (MSAlg_join U0) . x,y = (MSAlg_join U0) . y,x

proof

let x, y be Element of MSSub U0; :: thesis: (MSAlg_join U0) . x,y = (MSAlg_join U0) . y,x
reconsider U1 = x, U2 = y as strict MSSubAlgebra of U0 by Def20;
A1: ( (MSAlg_join U0) . x,y = U1 "\/" U2 & (MSAlg_join U0) . y,x = U2 "\/" U1 ) by Def21;
set B = the Sorts of U1 \/ the Sorts of U2;
( the Sorts of U1 is MSSubset of U0 & the Sorts of U2 is MSSubset of U0 ) by Def10;
then ( the Sorts of U1 c= the Sorts of U0 & the Sorts of U2 c= the Sorts of U0 ) by PBOOLE:def 23;
then the Sorts of U1 \/ the Sorts of U2 c= the Sorts of U0 by PBOOLE:18;
then reconsider B = the Sorts of U1 \/ the Sorts of U2 as MSSubset of U0 by PBOOLE:def 23;
( U1 "\/" U2 = GenMSAlg B & U2 "\/" U1 = GenMSAlg B ) by Def19;
hence (MSAlg_join U0) . x,y = (MSAlg_join U0) . y,x by A1; :: thesis: verum

end;

hence MSAlg_join U0 is commutative by BINOP_1:def 2; :: thesis: verum