for U0 being with_const_op Universal_Algebra holds the carrier of (UnSubAlLattice U0) = Sub U0 ;