for L being finite distributive LATTICE holds L, InclPoset (LOWER (subrelstr (Join-IRR L))) are_isomorphic