let U0 be with_const_op Universal_Algebra; :: thesis: for U1 being strict SubAlgebra of U0 holds Constants U0 c= (Carr U0) . U1

let U1 be strict SubAlgebra of U0; :: thesis: Constants U0 c= (Carr U0) . U1

U1 in Sub U0 by Th1;

then A1: (Carr U0) . U1 = the carrier of U1 by Def4;

Constants U1 = Constants U0 by Th6;

hence Constants U0 c= (Carr U0) . U1 by A1; :: thesis: verum

let U1 be strict SubAlgebra of U0; :: thesis: Constants U0 c= (Carr U0) . U1

U1 in Sub U0 by Th1;

then A1: (Carr U0) . U1 = the carrier of U1 by Def4;

Constants U1 = Constants U0 by Th6;

hence Constants U0 c= (Carr U0) . U1 by A1; :: thesis: verum