let U0 be with_const_op Universal_Algebra; :: thesis: for U1, U2 being SubAlgebra of U0 holds Constants U1 = Constants U2
let U1, U2 be SubAlgebra of U0; :: thesis: Constants U1 = Constants U2
Constants U0 = Constants U1 by Th6;
hence Constants U1 = Constants U2 by Th6; :: thesis: verum