let U0 be with_const_op Universal_Algebra; :: thesis: for U1, U2 being strict SubAlgebra of U0 holds (U1 /\ U2) "\/" U2 = U2

let U1, U2 be strict SubAlgebra of U0; :: thesis: (U1 /\ U2) "\/" U2 = U2

reconsider u12 = the carrier of (U1 /\ U2), u2 = the carrier of U2 as non empty Subset of U0 by Def7;

reconsider A = u12 \/ u2 as non empty Subset of U0 ;

the carrier of U1 meets the carrier of U2 by Th17;

then u12 = the carrier of U1 /\ the carrier of U2 by Def9;

then A1: u12 c= u2 by XBOOLE_1:17;

(U1 /\ U2) "\/" U2 = GenUnivAlg A by Def13;

hence (U1 /\ U2) "\/" U2 = U2 by A1, Th19, XBOOLE_1:12; :: thesis: verum

let U1, U2 be strict SubAlgebra of U0; :: thesis: (U1 /\ U2) "\/" U2 = U2

reconsider u12 = the carrier of (U1 /\ U2), u2 = the carrier of U2 as non empty Subset of U0 by Def7;

reconsider A = u12 \/ u2 as non empty Subset of U0 ;

the carrier of U1 meets the carrier of U2 by Th17;

then u12 = the carrier of U1 /\ the carrier of U2 by Def9;

then A1: u12 c= u2 by XBOOLE_1:17;

(U1 /\ U2) "\/" U2 = GenUnivAlg A by Def13;

hence (U1 /\ U2) "\/" U2 = U2 by A1, Th19, XBOOLE_1:12; :: thesis: verum