for U0 being strict with_const_op Universal_Algebra holds UnSubAlLattice U0 is bounded