for L being Boolean LATTICE
for x, a being Element of L st a is atom holds
( a <= x iff not a <= 'not' x )