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: 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)

let U0 be non-empty MSAlgebra over 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

hence
MSAlg_join U0 is commutative
by BINOP_1:def 2; :: thesis: verum
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 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 A1, PBOOLE:16;

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 & (MSAlg_join U0) . (y,x) = U2 "\/" U1 ) by Def20;

hence (MSAlg_join U0) . (x,y) = (MSAlg_join U0) . (y,x) by A2, Def18; :: thesis: verum

end;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 A1, PBOOLE:16;

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 & (MSAlg_join U0) . (y,x) = U2 "\/" U1 ) by Def20;

hence (MSAlg_join U0) . (x,y) = (MSAlg_join U0) . (y,x) by A2, Def18; :: thesis: verum