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