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 Def8;
reconsider A = u12 \/ u2 as non empty Subset of U0 ;
A1: (U1 /\ U2) "\/" U2 = GenUnivAlg A by Def14;
the carrier of U1 meets the carrier of U2 by Th20;
then u12 = the carrier of U1 /\ the carrier of U2 by Def10;
then u12 c= u2 by XBOOLE_1:17;
hence (U1 /\ U2) "\/" U2 = U2 by A1, Th22, XBOOLE_1:12; :: thesis: verum