:: deftheorem defines co-atomic LATTICE6:def 11 :
for L being Lattice
for a being Element of L holds
( a is co-atomic iff a is-lower-neighbour-of Top L );