for U0 being strict with_const_op Universal_Algebra
for H being Subset of U0 st H = the carrier of U0 holds
Top (UnSubAlLattice U0) = GenUnivAlg H