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