:: deftheorem defines MIRRS LATTICE6:def 15 :
for L being complete Lattice holds MIRRS L = { a where a is Element of L : a is completely-meet-irreducible } ;