let U0 be strict with_const_op Universal_Algebra; :: thesis:
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) ;

let l be Element of (UnSubAlLattice U0); :: thesis:
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:
hence l "/\" l1 = l1 ; :: thesis:

end;

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