let L be finite distributive LATTICE; 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; ( 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
; 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;
( 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
assume
not
Y is
empty
;
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;
( t in Y iff ( t < x & not t <= z ) )
(
t in Y implies (
t < x & not
t <= z ) )
proof
assume
t in Y
;
( 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 )
;
verum
end;
hence
(
t in Y iff (
t < x & not
t <= z ) )
by A4;
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;
verum
end;
assume
(
y < x & not
y <= z )
;
contradiction
then
y in Y
by A4;
hence
contradiction
by A5;
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; verum