let L be finite distributive LATTICE; :: thesis: for x being Element of L holds sup ((downarrow x) /\ (Join-IRR L)) = x

let x be Element of L; :: thesis: sup ((downarrow x) /\ (Join-IRR L)) = x

A1: x <= sup ((downarrow x) /\ (Join-IRR L))

then sup ((downarrow x) /\ (Join-IRR L)) <= sup (downarrow x) by XBOOLE_1:17, YELLOW_0:34;

then sup ((downarrow x) /\ (Join-IRR L)) <= x by WAYBEL_0:34;

hence sup ((downarrow x) /\ (Join-IRR L)) = x by A1, ORDERS_2:2; :: thesis: verum

let x be Element of L; :: thesis: sup ((downarrow x) /\ (Join-IRR L)) = x

A1: x <= sup ((downarrow x) /\ (Join-IRR L))

proof

( ex_sup_of (downarrow x) /\ (Join-IRR L),L & ex_sup_of downarrow x,L )
by YELLOW_0:17;
defpred S_{1}[ Element of L] means sup ((downarrow $1) /\ (Join-IRR L)) = $1;

A2: for x being Element of L st ( for b being Element of L st b < x holds

S_{1}[b] ) holds

S_{1}[x]
by Lm1;

for x being Element of L holds S_{1}[x]
from LATTICE7:sch 1(A2);

hence x <= sup ((downarrow x) /\ (Join-IRR L)) ; :: thesis: verum

end;A2: for x being Element of L st ( for b being Element of L st b < x holds

S

S

for x being Element of L holds S

hence x <= sup ((downarrow x) /\ (Join-IRR L)) ; :: thesis: verum

then sup ((downarrow x) /\ (Join-IRR L)) <= sup (downarrow x) by XBOOLE_1:17, YELLOW_0:34;

then sup ((downarrow x) /\ (Join-IRR L)) <= x by WAYBEL_0:34;

hence sup ((downarrow x) /\ (Join-IRR L)) = x by A1, ORDERS_2:2; :: thesis: verum