:: deftheorem defines Join-IRR LATTICE7:def 6 :
for L being LATTICE holds Join-IRR L = { a where a is Element of L : ( a <> Bottom L & ( for b, c being Element of L holds
( not a = b "\/" c or a = b or a = c ) ) ) } ;