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