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

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