:: deftheorem defines JIRRS LATTICE6:def 16 :
for L being complete Lattice holds JIRRS L = { a where a is Element of L : a is completely-join-irreducible } ;