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))

proof

defpred S₁[ 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₁[b] ) holds
S₁[x] by Lm1;
for x being Element of L holds S₁[x] from LATTICE7:sch 1(A2);
hence x <= sup ((downarrow x) /\ (Join-IRR L)) ; :: thesis: verum

end;

( ex_sup_of (downarrow x) /\ (Join-IRR L),L & ex_sup_of downarrow x,L ) by YELLOW_0:17;
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