theorem Th12: :: LATTICE7:12

for L being finite distributive LATTICE
for x being Element of L holds sup ((downarrow x) /\ (Join-IRR L)) = x