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

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