:: deftheorem defines preserves_complement LATTICE4:def 7 :
for L1, L2 being Lattice
for f being Homomorphism of L1,L2 holds
( f preserves_complement iff for a1 being Element of L1 holds f . (a1 `) = (f . a1) ` );