let L2 be Lattice; :: thesis: for 0L being lower-bounded Lattice
for f being Homomorphism of 0L,L2 st f is onto holds
( L2 is lower-bounded & f preserves_bottom )
let 0L be lower-bounded Lattice; :: thesis: for f being Homomorphism of 0L,L2 st f is onto holds
( L2 is lower-bounded & f preserves_bottom )
let f be Homomorphism of 0L,L2; :: thesis: ( f is onto implies ( L2 is lower-bounded & f preserves_bottom ) )
set r = f . (Bottom 0L);
assume A1: f is onto ; :: thesis: ( L2 is lower-bounded & f preserves_bottom )

A2: now

let a2 be Element of L2; :: thesis: ( (f . (Bottom 0L)) "/\" a2 = f . (Bottom 0L) & a2 "/\" (f . (Bottom 0L)) = f . (Bottom 0L) )
consider a1 being Element of 0L such that
A3: f . a1 = a2 by A1, Th9;
thus (f . (Bottom 0L)) "/\" a2 = f . ((Bottom 0L) "/\" a1) by A3, Def1
.= f . (Bottom 0L) by LATTICES:15 ; :: thesis: a2 "/\" (f . (Bottom 0L)) = f . (Bottom 0L)
hence a2 "/\" (f . (Bottom 0L)) = f . (Bottom 0L) ; :: thesis: verum

end;

thus L2 is lower-bounded :: thesis: f preserves_bottom

proof

take f . (Bottom 0L) ; :: according to LATTICES:def 13 :: thesis: for b₁ being Element of the carrier of L2 holds
( (f . (Bottom 0L)) "/\" b₁ = f . (Bottom 0L) & b₁ "/\" (f . (Bottom 0L)) = f . (Bottom 0L) )
thus for b₁ being Element of the carrier of L2 holds
( (f . (Bottom 0L)) "/\" b₁ = f . (Bottom 0L) & b₁ "/\" (f . (Bottom 0L)) = f . (Bottom 0L) ) by A2; :: thesis: verum

end;

then Bottom L2 = f . (Bottom 0L) by A2, LATTICES:def 16;
hence f preserves_bottom by Def8; :: thesis: verum