theorem Th6: :: UNIALG_3:6
for U0 being with_const_op Universal_Algebra
for U1 being SubAlgebra of U0 holds Constants U0 = Constants U1