theorem Th15: :: LATTICE7:15

for L being finite LATTICE holds LOWER (subrelstr (Join-IRR L)) is Ring_of_sets