let L be finite LATTICE; :: thesis: for y being Element of L st y <> Bottom L holds
ex x being Element of L st x <(1) y
let y be Element of L; :: thesis: ( y <> Bottom L implies ex x being Element of L st x <(1) y )
assume A1: y <> Bottom L ; :: thesis: ex x being Element of L st x <(1) y
( ex A being Chain of Bottom L,y st height y = card A & ( for A being Chain of Bottom L,y holds card A <= height y ) ) by Def3;
then consider A being Chain of Bottom L,y such that
A2: ( height y = card A & ( for A being Chain of Bottom L,y holds card A <= height y ) ) ;
set B = A \ {y};
A3: A \ {y} is strongly_connected Subset of L

proof

the InternalRel of L is_strongly_connected_in A \ {y}

proof

let p, q be set ; :: according to RELAT_2:def 7 :: thesis: ( not p in A \ {y} or not q in A \ {y} or [p,q] in the InternalRel of L or [q,p] in the InternalRel of L )
( p in A \ {y} & q in A \ {y} & not [p,q] in the InternalRel of L implies [q,p] in the InternalRel of L )

proof

assume A4: ( p in A \ {y} & q in A \ {y} ) ; :: thesis: ( [p,q] in the InternalRel of L or [q,p] in the InternalRel of L )
then A5: ( p in A & not p in {y} & q in A & not q in {y} ) by XBOOLE_0:def 5;
reconsider p = p, q = q as Element of L by A4;
( p <= q or q <= p ) by A5, ORDERS_2:38;
hence ( [p,q] in the InternalRel of L or [q,p] in the InternalRel of L ) by ORDERS_2:def 9; :: thesis: verum

end;

hence ( not p in A \ {y} or not q in A \ {y} or [p,q] in the InternalRel of L or [q,p] in the InternalRel of L ) ; :: thesis: verum

end;

hence A \ {y} is strongly_connected Subset of L by ORDERS_2:def 11; :: thesis: verum

end;

not A \ {y} is empty

proof

assume A6: A \ {y} is empty ; :: thesis: contradiction
Bottom L <= y by YELLOW_0:44;
then A7: Bottom L in A by Def2;
not Bottom L in {y} by A1, TARSKI:def 1;
hence contradiction by A6, A7, XBOOLE_0:def 5; :: thesis: verum

end;

then reconsider B = A \ {y} as non empty Chain of L by A3;
take x = max B; :: thesis: x <(1) y
A8: x < y

proof

A9: x in B by Def5;
A10: Bottom L <= y by YELLOW_0:44;
( x in A & not x in {y} ) by A9, XBOOLE_0:def 5;
then ( Bottom L <= x & x <= y & not x = y ) by A10, Def2, TARSKI:def 1;
hence x < y by ORDERS_2:def 10; :: thesis: verum

end;

for z being Element of L holds
( not x < z or not z < y )

proof

given z being Element of L such that A11: ( x < z & z < y ) ; :: thesis: contradiction
A12: not z in A

proof

assume A13: z in A ; :: thesis: contradiction
not z in {y} by A11, TARSKI:def 1;
then z in B by A13, XBOOLE_0:def 5;
then ( z <= x & x < z ) by A11, Def5;
hence contradiction by ORDERS_2:32; :: thesis: verum

end;

set C = A \/ {z};
A14: A \/ {z} is strongly_connected Subset of L

proof

A15: A = (A \ {y}) \/ {y}

proof

{y} c= A

proof

let h be Element of L; :: according to LATTICE7:def 1 :: thesis: ( h in {y} implies h in A )
assume h in {y} ; :: thesis: h in A
then A16: h = y by TARSKI:def 1;
Bottom L <= y by YELLOW_0:44;
hence h in A by A16, Def2; :: thesis: verum

end;

hence A = (A \ {y}) \/ {y} by XBOOLE_1:45; :: thesis: verum

end;

the InternalRel of L is_strongly_connected_in A \/ {z}

proof

let x1, y1 be set ; :: according to RELAT_2:def 7 :: thesis: ( not x1 in A \/ {z} or not y1 in A \/ {z} or [x1,y1] in the InternalRel of L or [y1,x1] in the InternalRel of L )
( x1 in A \/ {z} & y1 in A \/ {z} & not [x1,y1] in the InternalRel of L implies [y1,x1] in the InternalRel of L )

proof

assume A17: ( x1 in A \/ {z} & y1 in A \/ {z} ) ; :: thesis: ( [x1,y1] in the InternalRel of L or [y1,x1] in the InternalRel of L )

per cases ( ( x1 in A & y1 in A ) or ( x1 in A & y1 in {z} ) or ( y1 in A & x1 in {z} ) or ( x1 in {z} & y1 in {z} ) ) by A17, XBOOLE_0:def 3;

suppose A18: ( x1 in A & y1 in A ) ; :: thesis: ( [x1,y1] in the InternalRel of L or [y1,x1] in the InternalRel of L )

then reconsider x1 = x1, y1 = y1 as Element of L ;
( x1 <= y1 or y1 <= x1 ) by A18, ORDERS_2:38;
hence ( [x1,y1] in the InternalRel of L or [y1,x1] in the InternalRel of L ) by ORDERS_2:def 9; :: thesis: verum

end;

suppose A19: ( x1 in A & y1 in {z} ) ; :: thesis: ( [x1,y1] in the InternalRel of L or [y1,x1] in the InternalRel of L )

then A20: y1 = z by TARSKI:def 1;
reconsider x1 = x1, y1 = y1 as Element of L by A19;
( x1 in A \ {y} or x1 in {y} ) by A15, A19, XBOOLE_0:def 3;
then ( x1 <= x or x1 = y ) by Def5, TARSKI:def 1;
then ( x1 < y1 or x1 = y ) by A11, A20, ORDERS_2:32;
then ( x1 <= y1 or y1 < x1 ) by A11, A19, ORDERS_2:def 10, TARSKI:def 1;
then ( x1 <= y1 or y1 <= x1 ) by ORDERS_2:def 10;
hence ( [x1,y1] in the InternalRel of L or [y1,x1] in the InternalRel of L ) by ORDERS_2:def 9; :: thesis: verum

end;

suppose A21: ( y1 in A & x1 in {z} ) ; :: thesis: ( [x1,y1] in the InternalRel of L or [y1,x1] in the InternalRel of L )

then A22: x1 = z by TARSKI:def 1;
reconsider x1 = x1, y1 = y1 as Element of L by A21;
( y1 in A \ {y} or y1 in {y} ) by A15, A21, XBOOLE_0:def 3;
then ( y1 <= x or y1 = y ) by Def5, TARSKI:def 1;
then ( y1 < x1 or y1 = y ) by A11, A22, ORDERS_2:32;
then ( y1 <= x1 or x1 <= y1 ) by A11, A22, ORDERS_2:def 10;
hence ( [x1,y1] in the InternalRel of L or [y1,x1] in the InternalRel of L ) by ORDERS_2:def 9; :: thesis: verum

end;

suppose A23: ( x1 in {z} & y1 in {z} ) ; :: thesis: ( [x1,y1] in the InternalRel of L or [y1,x1] in the InternalRel of L )

then reconsider x1 = x1, y1 = y1 as Element of L ;
( x1 = z & y1 = z ) by A23, TARSKI:def 1;
then x1 <= y1 ;
hence ( [x1,y1] in the InternalRel of L or [y1,x1] in the InternalRel of L ) by ORDERS_2:def 9; :: thesis: verum

end;

end;

end;

hence ( not x1 in A \/ {z} or not y1 in A \/ {z} or [x1,y1] in the InternalRel of L or [y1,x1] in the InternalRel of L ) ; :: thesis: verum

end;

hence A \/ {z} is strongly_connected Subset of L by ORDERS_2:def 11; :: thesis: verum

end;

A24: Bottom L <= y by YELLOW_0:44;
then A25: Bottom L in A by Def2;
A26: y in A by A24, Def2;
A27: Bottom L in A \/ {z} by A25, XBOOLE_0:def 3;
A28: y in A \/ {z} by A26, XBOOLE_0:def 3;
A29: ( Bottom L <= z & z <= y ) by A11, ORDERS_2:def 10, YELLOW_0:44;
for v being Element of L st v in A \/ {z} holds
( Bottom L <= v & v <= y )

proof

let v be Element of L; :: thesis: ( v in A \/ {z} implies ( Bottom L <= v & v <= y ) )
assume A30: v in A \/ {z} ; :: thesis: ( Bottom L <= v & v <= y )

per cases ( v in A or v in {z} ) by A30, XBOOLE_0:def 3;

suppose A31: v in A ; :: thesis: ( Bottom L <= v & v <= y )

thus Bottom L <= v by YELLOW_0:44; :: thesis: v <= y
thus v <= y by A24, A31, Def2; :: thesis: verum

end;

suppose v in {z} ; :: thesis: ( Bottom L <= v & v <= y )

hence ( Bottom L <= v & v <= y ) by A29, TARSKI:def 1; :: thesis: verum

end;

end;

end;

then A32: A \/ {z} is Chain of Bottom L,y by A14, A24, A27, A28, Def2;
card (A \/ {z}) = (card A) + 1 by A12, CARD_2:54;
then (card A) + 1 <= card A by A2, A32;
hence contradiction by NAT_1:13; :: thesis: verum

end;

hence x <(1) y by A8, Def4; :: thesis: verum