:: deftheorem defines preserves_bottom LATTICE4:def 6 :
for L1, L2 being Lattice
for f being Homomorphism of L1,L2 holds
( f preserves_bottom iff f . (Bottom L1) = Bottom L2 );