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 A6, Th8;
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 A3, ORDERS_2:def 6;
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 A11, YELLOW_5:9;
then A13: a "\/" z < x by A12, ORDERS_2:def 6;
a "/\" a <= a "\/" z by YELLOW_5:5;
then A14: a <= a "\/" z by YELLOW_5:2;
a <> a "\/" z then A15: a "\/" z > a by A14, ORDERS_2:def 6;
not a "\/" z <= z by A10, YELLOW_5:3;
then a "\/" z in Y by A9, A13;
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