let L be finite distributive LATTICE; :: thesis: L, InclPoset (LOWER (subrelstr (Join-IRR L))) are_isomorphic
ex r being Function of L,(InclPoset (LOWER (subrelstr (Join-IRR L)))) st
( r is isomorphic & ( for a being Element of L holds r . a = (downarrow a) /\ (Join-IRR L) ) ) by Th13;
hence L, InclPoset (LOWER (subrelstr (Join-IRR L))) are_isomorphic ; :: thesis: verum