:: deftheorem defines preserves_top LATTICE4:def 4 :
for L1, L2 being Lattice
for f being Homomorphism of L1,L2 holds
( f preserves_top iff f . (Top L1) = Top L2 );