let U0 be strict with_const_op Universal_Algebra; :: thesis: for H being Subset of U0 st H = the carrier of U0 holds
Top (UnSubAlLattice U0) = GenUnivAlg H
let H be Subset of U0; :: thesis: ( H = the carrier of U0 implies Top (UnSubAlLattice U0) = GenUnivAlg H )
set L = UnSubAlLattice U0;
reconsider u1 = GenUnivAlg H as Element of Sub U0 by UNIALG_2:def 14;
reconsider l1 = u1 as Element of (UnSubAlLattice U0) ;
assume A1: H = the carrier of U0 ; :: thesis: Top (UnSubAlLattice U0) = GenUnivAlg H
now :: thesis: for l being Element of (UnSubAlLattice U0) holds
( l1 "\/" l = l1 & l "\/" l1 = l1 )
let l be Element of (UnSubAlLattice U0); :: thesis: ( l1 "\/" l = l1 & l "\/" l1 = l1 )
reconsider u2 = l as Element of Sub U0 ;
reconsider U2 = u2 as strict SubAlgebra of U0 by UNIALG_2:def 14;
thus l1 "\/" l = (GenUnivAlg H) "\/" U2 by UNIALG_2:def 15
.= l1 by A1, Th20 ; :: thesis: l "\/" l1 = l1
hence l "\/" l1 = l1 ; :: thesis: verum
end;
hence Top (UnSubAlLattice U0) = GenUnivAlg H by LATTICES:def 17; :: thesis: verum