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