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 Def14;
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 Def7;
then reconsider B = B as non empty Subset of U0 by XBOOLE_1:8;
A1: U1 "\/" U2 = GenUnivAlg B by Def13;
( (UniAlg_join U0) . (x,y) = U1 "\/" U2 & (UniAlg_join U0) . (y,x) = U2 "\/" U1 ) by Def15;
hence (UniAlg_join U0) . (x,y) = (UniAlg_join U0) . (y,x) by A1, Def13; :: thesis: verum

end;

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