for U0 being Universal_Algebra
for u being object holds
( u in Sub U0 iff ex U1 being strict SubAlgebra of U0 st u = U1 )