let U0 be strict with_const_op Universal_Algebra; :: thesis: for U1 being strict SubAlgebra of U0 holds (GenUnivAlg (Constants U0)) /\ U1 = GenUnivAlg (Constants U0)
let U1 be strict SubAlgebra of U0; :: thesis: (GenUnivAlg (Constants U0)) /\ U1 = GenUnivAlg (Constants U0)
set C = Constants U0;
set G = GenUnivAlg (Constants U0);
Constants U0 is Subset of U1 by UNIALG_2:15;
then GenUnivAlg (Constants U0) is strict SubAlgebra of U1 by UNIALG_2:def 12;
then A1: the carrier of (GenUnivAlg (Constants U0)) is Subset of U1 by UNIALG_2:def 7;
the carrier of (GenUnivAlg (Constants U0)) meets the carrier of U1 by UNIALG_2:17;
then the carrier of ((GenUnivAlg (Constants U0)) /\ U1) = the carrier of (GenUnivAlg (Constants U0)) /\ the carrier of U1 by UNIALG_2:def 9;
hence (GenUnivAlg (Constants U0)) /\ U1 = GenUnivAlg (Constants U0) by A1, UNIALG_2:12, XBOOLE_1:28; :: thesis: verum