let L be finite distributive LATTICE; :: thesis: L, InclPoset (LOWER (subrelstr (Join-IRR L))) are_isomorphic
consider r being Function of L,(InclPoset (LOWER (subrelstr (Join-IRR L)))) such that
A1: ( r is isomorphic & ( for a being Element of L holds r . a = (downarrow a) /\ (Join-IRR L) ) ) by Th13;
thus L, InclPoset (LOWER (subrelstr (Join-IRR L))) are_isomorphic by A1, WAYBEL_1:def 8; :: thesis: verum