let U0 be strict with_const_op Universal_Algebra; :: thesis: Top (UnSubAlLattice U0) = U0
A1: U0 is strict SubAlgebra of U0 by UNIALG_2:8;
the carrier of U0 c= the carrier of U0 ;
then reconsider H = the carrier of U0 as Subset of U0 ;
thus Top (UnSubAlLattice U0) = GenUnivAlg H by Th21
.= U0 by A1, UNIALG_2:19 ; :: thesis: verum