let S be non empty non void ManySortedSign ; for U0 being non-empty MSAlgebra of S holds MSAlg_join U0 is commutative
let U0 be non-empty MSAlgebra of S; 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;
(MSAlg_join U0) . x,y = (MSAlg_join U0) . y,x
reconsider U1 =
x,
U2 =
y as
strict MSSubAlgebra of
U0 by Def20;
set B = the
Sorts of
U1 \/ the
Sorts of
U2;
the
Sorts of
U2 is
MSSubset of
U0
by Def10;
then A1:
the
Sorts of
U2 c= the
Sorts of
U0
by PBOOLE:def 23;
the
Sorts of
U1 is
MSSubset of
U0
by Def10;
then
the
Sorts of
U1 c= the
Sorts of
U0
by PBOOLE:def 23;
then
the
Sorts of
U1 \/ the
Sorts of
U2 c= the
Sorts of
U0
by A1, PBOOLE:18;
then reconsider B = the
Sorts of
U1 \/ the
Sorts of
U2 as
MSSubset of
U0 by PBOOLE:def 23;
A2:
U1 "\/" U2 = GenMSAlg B
by Def19;
(
(MSAlg_join U0) . x,
y = U1 "\/" U2 &
(MSAlg_join U0) . y,
x = U2 "\/" U1 )
by Def21;
hence
(MSAlg_join U0) . x,
y = (MSAlg_join U0) . y,
x
by A2, Def19;
verum
end;
hence
MSAlg_join U0 is commutative
by BINOP_1:def 2; verum