let L be finite distributive LATTICE; :: thesis: for x being Element of L st x in Join-IRR L holds
ex z being Element of L st
( z < x & ( for y being Element of L st y < x holds
y <= z ) )

let x be Element of L; :: thesis: ( x in Join-IRR L implies ex z being Element of L st
( z < x & ( for y being Element of L st y < x holds
y <= z ) ) )

assume A1: x in Join-IRR L ; :: thesis: ex z being Element of L st
( z < x & ( for y being Element of L st y < x holds
y <= z ) )

then x <> Bottom L by Th10;
then consider z being Element of L such that
A2: z <(1) x by Th9;
A3: z < x by A2;
for y being Element of L st y < x holds
y <= z
proof
let y be Element of L; :: thesis: ( y < x implies y <= z )
consider Y being set such that
A4: Y = { g where g is Element of L : ( g < x & not g <= z ) } ;
A5: Y is empty
proof
A6: Y c= the carrier of L
proof
let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in Y or f in the carrier of L )
assume f in Y ; :: thesis: f in the carrier of L
then ex g being Element of L st
( g = f & g < x & not g <= z ) by A4;
hence f in the carrier of L ; :: thesis: verum
end;
assume not Y is empty ; :: thesis: contradiction
then consider a being Element of L such that
A7: a in Y and
A8: for b being Element of L st b in Y holds
not a < b by ;
A9: for t being Element of L holds
( t in Y iff ( t < x & not t <= z ) )
proof
let t be Element of L; :: thesis: ( t in Y iff ( t < x & not t <= z ) )
( t in Y implies ( t < x & not t <= z ) )
proof
assume t in Y ; :: thesis: ( t < x & not t <= z )
then ex g being Element of L st
( g = t & g < x & not g <= z ) by A4;
hence ( t < x & not t <= z ) ; :: thesis: verum
end;
hence ( t in Y iff ( t < x & not t <= z ) ) by A4; :: thesis: verum
end;
then A10: not a <= z by A7;
A11: z <= x by ;
a < x by A9, A7;
then A12: a "\/" z <> x by A1, A3, Th10;
a < x by A9, A7;
then a <= x by ORDERS_2:def 6;
then a "\/" z <= x by ;
then A13: a "\/" z < x by ;
a "/\" a <= a "\/" z by YELLOW_5:5;
then A14: a <= a "\/" z by YELLOW_5:2;
a <> a "\/" z
proof
assume a = a "\/" z ; :: thesis: contradiction
z "/\" z <= a "\/" z by YELLOW_5:5;
then z <= a "\/" z by YELLOW_5:2;
then z < a "\/" z by ;
hence contradiction by A2, A13; :: thesis: verum
end;
then A15: a "\/" z > a by ;
not a "\/" z <= z by ;
then a "\/" z in Y by ;
hence contradiction by A8, A15; :: thesis: verum
end;
assume ( y < x & not y <= z ) ; :: thesis: contradiction
then y in Y by A4;
hence contradiction by A5; :: thesis: verum
end;
hence ex z being Element of L st
( z < x & ( for y being Element of L st y < x holds
y <= z ) ) by A3; :: thesis: verum