for U0 being Universal_Algebra
for H being strict SubAlgebra of U0
for u being Element of U0 holds
( u in (Carr U0) . H iff u in H )