theorem Th10: :: LATTICE7:10

for L being LATTICE
for x being Element of L holds
( x in Join-IRR L iff ( x <> Bottom L & ( for b, c being Element of L holds
( not x = b "\/" c or x = b or x = c ) ) ) )