let U0 be strict with_const_op Universal_Algebra; :: thesis: Bottom (UnSubAlLattice U0) = GenUnivAlg (Constants U0)

set L = UnSubAlLattice U0;

set C = Constants U0;

reconsider G = GenUnivAlg (Constants U0) as Element of Sub U0 by UNIALG_2:def 14;

reconsider l1 = G as Element of (UnSubAlLattice U0) ;

set L = UnSubAlLattice U0;

set C = Constants U0;

reconsider G = GenUnivAlg (Constants U0) as Element of Sub U0 by UNIALG_2:def 14;

reconsider l1 = G as Element of (UnSubAlLattice U0) ;

now :: thesis: for l being Element of (UnSubAlLattice U0) holds

( l1 "/\" l = l1 & l "/\" l1 = l1 )

hence
Bottom (UnSubAlLattice U0) = GenUnivAlg (Constants U0)
by LATTICES:def 16; :: thesis: verum( l1 "/\" l = l1 & l "/\" l1 = l1 )

let l be Element of (UnSubAlLattice U0); :: thesis: ( l1 "/\" l = l1 & l "/\" l1 = l1 )

reconsider u1 = l as Element of Sub U0 ;

reconsider U2 = u1 as strict SubAlgebra of U0 by UNIALG_2:def 14;

thus l1 "/\" l = (GenUnivAlg (Constants U0)) /\ U2 by UNIALG_2:def 16

.= l1 by Th18 ; :: thesis: l "/\" l1 = l1

hence l "/\" l1 = l1 ; :: thesis: verum

end;reconsider u1 = l as Element of Sub U0 ;

reconsider U2 = u1 as strict SubAlgebra of U0 by UNIALG_2:def 14;

thus l1 "/\" l = (GenUnivAlg (Constants U0)) /\ U2 by UNIALG_2:def 16

.= l1 by Th18 ; :: thesis: l "/\" l1 = l1

hence l "/\" l1 = l1 ; :: thesis: verum