theorem Th15: :: UNIALG_3:15

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 the carrier of U1 c= the carrier of U2 )