theorem :: UNIALG_3:10

for U0 being with_const_op Universal_Algebra
for U1 being strict SubAlgebra of U0 holds Constants U0 c= (Carr U0) . U1