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

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