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

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 )

hence
Top (UnSubAlLattice U0) = GenUnivAlg H
by LATTICES:def 17; :: thesis: verum( 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;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