for U0 being strict with_const_op Universal_Algebra holds Top (UnSubAlLattice U0) = U0