theorem :: UNIALG_3:23

for U0 being strict with_const_op Universal_Algebra holds UnSubAlLattice U0 is complete