for U0 being with_const_op Universal_Algebra
for l1, l2 being Element of (UnSubAlLattice U0)
for U1, U2 being strict SubAlgebra of U0 st l1 = U1 & l2 = U2 holds
( l1 [= l2 iff U1 is SubAlgebra of U2 )