theorem :: UNIALG_3:22

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