let S be non empty non void ManySortedSign ; :: thesis: for U0 being non-empty MSAlgebra over S holds MSAlg_join U0 is commutative
let U0 be non-empty MSAlgebra over S; :: thesis:
set o = MSAlg_join U0;
for x, y being Element of MSSub U0 holds () . (x,y) = () . (y,x)
proof
let x, y be Element of MSSub U0; :: thesis: () . (x,y) = () . (y,x)
reconsider U1 = x, U2 = y as strict MSSubAlgebra of U0 by Def19;
set B = the Sorts of U1 (\/) the Sorts of U2;
the Sorts of U2 is MSSubset of U0 by Def9;
then A1: the Sorts of U2 c= the Sorts of U0 by PBOOLE:def 18;
the Sorts of U1 is MSSubset of U0 by Def9;
then the Sorts of U1 c= the Sorts of U0 by PBOOLE:def 18;
then the Sorts of U1 (\/) the Sorts of U2 c= the Sorts of U0 by ;
then reconsider B = the Sorts of U1 (\/) the Sorts of U2 as MSSubset of U0 by PBOOLE:def 18;
A2: U1 "\/" U2 = GenMSAlg B by Def18;
( (MSAlg_join U0) . (x,y) = U1 "\/" U2 & () . (y,x) = U2 "\/" U1 ) by Def20;
hence (MSAlg_join U0) . (x,y) = () . (y,x) by ; :: thesis: verum
end;
hence MSAlg_join U0 is commutative by BINOP_1:def 2; :: thesis: verum