:: deftheorem defines atomic LATTICE6:def 12 :
for L being Lattice holds
( L is atomic iff for a being Element of L ex X being Subset of L st
( ( for x being Element of L st x in X holds
x is atomic ) & a = "\/" (X,L) ) );