let U0 be Universal_Algebra; :: thesis: UniAlg_join U0 is commutative
set o = UniAlg_join U0;
for x, y being Element of Sub U0 holds (UniAlg_join U0) . x,y = (UniAlg_join U0) . y,x

proof

let x, y be Element of Sub U0; :: thesis: (UniAlg_join U0) . x,y = (UniAlg_join U0) . y,x
reconsider U1 = x, U2 = y as strict SubAlgebra of U0 by Def15;
A1: ( (UniAlg_join U0) . x,y = U1 "\/" U2 & (UniAlg_join U0) . y,x = U2 "\/" U1 ) by Def16;
reconsider B = the carrier of U1 \/ the carrier of U2 as non empty set ;
( the carrier of U1 is Subset of U0 & the carrier of U2 is Subset of U0 ) by Def8;
then reconsider B = B as non empty Subset of U0 by XBOOLE_1:8;
( U1 "\/" U2 = GenUnivAlg B & U2 "\/" U1 = GenUnivAlg B ) by Def14;
hence (UniAlg_join U0) . x,y = (UniAlg_join U0) . y,x by A1; :: thesis: verum

end;

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