theorem Th11: :: LATTICE7:11

for L being finite distributive LATTICE
for x being Element of L st x in Join-IRR L holds
ex z being Element of L st
( z < x & ( for y being Element of L st y < x holds
y <= z ) )