let U0 be Universal_Algebra; :: thesis: for U1, U2 being SubAlgebra of U0 holds U1 "\/" U2 = U2 "\/" U1
let U1, U2 be SubAlgebra of U0; :: thesis: U1 "\/" U2 = U2 "\/" U1
reconsider u1 = the carrier of U1, u2 = the carrier of U2 as non empty Subset of U0 by Def7;
reconsider A = u1 \/ u2 as non empty Subset of U0 ;
U1 "\/" U2 = GenUnivAlg A by Def13;
hence U1 "\/" U2 = U2 "\/" U1 by Def13; :: thesis: verum