:: deftheorem defines completely-join-irreducible LATTICE6:def 9 :
for L being complete Lattice
for a being Element of L holds
( a is completely-join-irreducible iff *' a <> a );