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 & ( for b, c being Element of L holds
( not x = b "\/" c or x = b or x = c ) ) ) by Th10;
then consider z being Element of L such that
A2: z <(1) x by Th9;
A3: ( z < x & ( for v being Element of L holds
( not z < v or not v < x ) ) ) by A2, Def4;
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 )
assume A4: ( y < x & not y <= z ) ; :: thesis: contradiction
consider Y being set such that
A5: Y = { g where g is Element of L : ( g < x & not g <= z ) } ;
A6: Y is empty

proof

assume A7: not Y is empty ; :: thesis: contradiction
A8: 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 consider g being Element of L such that
A9: ( g = t & g < x & not g <= z ) by A5;
thus ( t < x & not t <= z ) by A9; :: thesis: verum

end;

hence ( t in Y iff ( t < x & not t <= z ) ) by A5; :: thesis: verum

end;

Y is Subset of L

proof

Y c= the carrier of L

proof

let f be set ; :: 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 consider g being Element of L such that
A10: ( g = f & g < x & not g <= z ) by A5;
thus f in the carrier of L by A10; :: thesis: verum

end;

hence Y is Subset of L ; :: thesis: verum
thus verum ; :: thesis: verum

end;

then consider a being Element of L such that
A11: a in Y and
A12: for b being Element of L st b in Y holds
not a < b by A7, Th8;
A13: ( a < x & not a <= z ) by A8, A11;
A14: a "\/" z < x

proof

a < x by A8, A11;
then A15: a <= x by ORDERS_2:def 10;
z <= x by A3, ORDERS_2:def 10;
then A16: a "\/" z <= x by A15, YELLOW_5:9;
a "\/" z <> x by A1, A3, A13, Th10;
hence a "\/" z < x by A16, ORDERS_2:def 10; :: thesis: verum

end;

not a "\/" z <= z by A13, YELLOW_5:3;
then A17: a "\/" z in Y by A8, A14;
a "\/" z > a

proof

a "/\" a <= a "\/" z by YELLOW_5:5;
then A18: a <= a "\/" z by YELLOW_5:2;
a <> a "\/" z

proof

assume a = a "\/" z ; :: thesis: contradiction
z < a "\/" z

proof

z "/\" z <= a "\/" z by YELLOW_5:5;
then z <= a "\/" z by YELLOW_5:2;
hence z < a "\/" z by A13, A18, ORDERS_2:def 10; :: thesis: verum

end;

hence contradiction by A2, A14, Def4; :: thesis: verum

end;

hence a "\/" z > a by A18, ORDERS_2:def 10; :: thesis: verum

end;

hence contradiction by A12, A17; :: thesis: verum

end;

y in Y by A4, A5;
hence contradiction by A6; :: 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