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