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

( z < x & ( for y being Element of L st y < x holds

y <= z ) ) by A3; :: thesis: verum

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

hence
ex z being Element of L st
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

then y in Y by A4;

hence contradiction by A5; :: thesis: verum

end;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

assume
( y < x & not y <= z )
; :: thesis: contradiction
A6:
Y c= the carrier of L

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

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

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;proof

assume
not Y is empty
; :: thesis: contradiction
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 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

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

then A10:
not a <= z
by A7;
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 ) )

end;( t in Y implies ( t < x & not t <= z ) )

proof

hence
( t in Y iff ( t < x & not t <= z ) )
by A4; :: thesis: verum
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;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

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

proof

then A15:
a "\/" z > a
by A14, ORDERS_2:def 6;
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 A10, A14, ORDERS_2:def 6;

hence contradiction by A2, A13; :: thesis: verum

end;z "/\" z <= a "\/" z by YELLOW_5:5;

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

then z < a "\/" z by A10, A14, ORDERS_2:def 6;

hence contradiction by A2, A13; :: thesis: verum

not a "\/" z <= z by A10, YELLOW_5:3;

then a "\/" z in Y by A9, A13;

hence contradiction by A8, A15; :: thesis: verum

then y in Y by A4;

hence contradiction by A5; :: thesis: verum

( z < x & ( for y being Element of L st y < x holds

y <= z ) ) by A3; :: thesis: verum