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 7 :: 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 that
A1: a in LOWER (subrelstr (Join-IRR L)) and
A2: b in LOWER (subrelstr (Join-IRR L)) ; :: thesis: ( a /\ b in LOWER (subrelstr (Join-IRR L)) & a \/ b in LOWER (subrelstr (Join-IRR L)) )
A3: a \/ b in LOWER (subrelstr (Join-IRR L))

proof

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

end;

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

proof

consider Z1 being Subset of (subrelstr (Join-IRR L)) such that
A8: b = Z1 and
A9: Z1 is lower by A2;
consider Z being Subset of (subrelstr (Join-IRR L)) such that
A10: a = Z and
A11: Z is lower by A1;
Z /\ Z1 is lower by A11, A9, WAYBEL_0:27;
hence a /\ b in LOWER (subrelstr (Join-IRR L)) by A10, A8; :: thesis: verum

end;

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

end;

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