theorem Th14: :: LATTICE7:14

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