let L be finite LATTICE; :: thesis: LOWER (subrelstr (Join-IRR L)) is Ring_of_sets
set X = LOWER (subrelstr (Join-IRR L));
LOWER (subrelstr (Join-IRR L)) includes_lattice_of LOWER (subrelstr (Join-IRR L))

proof

let a, b be set ; :: according to COHSP_1:def 8 :: thesis: ( not a in LOWER (subrelstr (Join-IRR L)) or not b in LOWER (subrelstr (Join-IRR L)) or ( a /\ b in LOWER (subrelstr (Join-IRR L)) & a \/ b in LOWER (subrelstr (Join-IRR L)) ) )
assume A1: ( a in LOWER (subrelstr (Join-IRR L)) & b in LOWER (subrelstr (Join-IRR L)) ) ; :: thesis: ( a /\ b in LOWER (subrelstr (Join-IRR L)) & a \/ b in LOWER (subrelstr (Join-IRR L)) )
A2: a /\ b in LOWER (subrelstr (Join-IRR L))

proof

consider Z being Subset of (subrelstr (Join-IRR L)) such that
A3: ( a = Z & Z is lower ) by A1;
consider Z1 being Subset of (subrelstr (Join-IRR L)) such that
A4: ( b = Z1 & Z1 is lower ) by A1;
Z /\ Z1 is lower by A3, A4, WAYBEL_0:27;
hence a /\ b in LOWER (subrelstr (Join-IRR L)) by A3, A4; :: thesis: verum

end;

a \/ b in LOWER (subrelstr (Join-IRR L))

proof

consider Z being Subset of (subrelstr (Join-IRR L)) such that
A5: ( a = Z & Z is lower ) by A1;
consider Z1 being Subset of (subrelstr (Join-IRR L)) such that
A6: ( b = Z1 & Z1 is lower ) by A1;
Z \/ Z1 is lower by A5, A6, WAYBEL_0:27;
hence a \/ b in LOWER (subrelstr (Join-IRR L)) by A5, A6; :: thesis: verum

end;

hence ( a /\ b in LOWER (subrelstr (Join-IRR L)) & a \/ b in LOWER (subrelstr (Join-IRR L)) ) by A2; :: thesis: verum

end;

hence LOWER (subrelstr (Join-IRR L)) is Ring_of_sets by Def8; :: thesis: verum