for U0 being Universal_Algebra
for U1 being SubAlgebra of U0 holds the carrier of U1 c= the carrier of U0