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) ;

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 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;

hence Bottom (UnSubAlLattice U0) = GenUnivAlg (Constants U0) by LATTICES:def 16; :: thesis: verum