theorem :: UNIALG_3:7

for U0 being with_const_op Universal_Algebra
for U1, U2 being SubAlgebra of U0 holds Constants U1 = Constants U2