let L be finite LATTICE; :: thesis:
let y be Element of L; :: thesis:
( 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
A1: ( height y = card A & ( for A being Chain of Bottom L,y holds card A <= height y ) ) ;
set B = A \ {y};
A2: the InternalRel of L is_strongly_connected_in A \ {y}

proof

let p, q be object ; :: according to RELAT_2:def 7 :: thesis:
( 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 A3: ( p in A \ {y} & q in A \ {y} ) ; :: thesis:
then A4: ( p in A & q in A ) by XBOOLE_0:def 5;
reconsider p = p, q = q as Element of L by A3;
( p <= q or q <= p ) by A4, ORDERS_2:11;
hence ( [p,q] in the InternalRel of L or [q,p] in the InternalRel of L ) by ORDERS_2:def 5; :: thesis:

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:

end;

assume A5: y <> Bottom L ; :: thesis:
not A \ {y} is empty

proof

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

end;

then reconsider B = A \ {y} as non empty Chain of L by A2, ORDERS_2:def 7;
take x = max B; :: thesis:
A8: for z being Element of L holds
( not x < z or not z < y )

proof

given z being Element of L such that A9: x < z and
A10: z < y ; :: thesis:
A11: Bottom L <= y by YELLOW_0:44;
then y in A by Def2;
then A12: y in A \/ {z} by XBOOLE_0:def 3;
set C = A \/ {z};
{y} c= A

proof

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

end;

then A14: A = (A \ {y}) \/ {y} by XBOOLE_1:45;
the InternalRel of L is_strongly_connected_in A \/ {z}

proof

let x1, y1 be object ; :: according to RELAT_2:def 7 :: thesis:
( 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 A15: ( x1 in A \/ {z} & y1 in A \/ {z} ) ; :: thesis:

per cases by A15, XBOOLE_0:def 3;

suppose A16: ( x1 in A & y1 in A ) ; :: thesis:

then reconsider x1 = x1, y1 = y1 as Element of L ;
( x1 <= y1 or y1 <= x1 ) by A16, ORDERS_2:11;
hence ( [x1,y1] in the InternalRel of L or [y1,x1] in the InternalRel of L ) by ORDERS_2:def 5; :: thesis:

end;

suppose A17: ( x1 in A & y1 in {z} ) ; :: thesis:

then A18: y1 = z by TARSKI:def 1;
reconsider x1 = x1, y1 = y1 as Element of L by A17;
( x1 in A \ {y} or x1 in {y} ) by A14, A17, XBOOLE_0:def 3;
then ( x1 <= x or x1 = y ) by Def5, TARSKI:def 1;
then ( x1 < y1 or x1 = y ) by A9, A18, ORDERS_2:7;
then ( x1 <= y1 or y1 < x1 ) by A10, A17, ORDERS_2:def 6, TARSKI:def 1;
then ( x1 <= y1 or y1 <= x1 ) by ORDERS_2:def 6;
hence ( [x1,y1] in the InternalRel of L or [y1,x1] in the InternalRel of L ) by ORDERS_2:def 5; :: thesis:

end;

suppose A19: ( y1 in A & x1 in {z} ) ; :: thesis:

then A20: x1 = z by TARSKI:def 1;
reconsider x1 = x1, y1 = y1 as Element of L by A19;
( y1 in A \ {y} or y1 in {y} ) by A14, A19, XBOOLE_0:def 3;
then ( y1 <= x or y1 = y ) by Def5, TARSKI:def 1;
then ( y1 < x1 or y1 = y ) by A9, A20, ORDERS_2:7;
then ( y1 <= x1 or x1 <= y1 ) by A10, A20, ORDERS_2:def 6;
hence ( [x1,y1] in the InternalRel of L or [y1,x1] in the InternalRel of L ) by ORDERS_2:def 5; :: thesis:

end;

suppose A21: ( x1 in {z} & y1 in {z} ) ; :: thesis:

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

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:

end;

then A22: A \/ {z} is strongly_connected Subset of L by ORDERS_2:def 7;
A23: z <= y by A10, ORDERS_2:def 6;
A24: 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:
assume A25: v in A \/ {z} ; :: thesis:

per cases by A25, XBOOLE_0:def 3;

suppose A26: v in A ; :: thesis:

thus Bottom L <= v by YELLOW_0:44; :: thesis:
thus v <= y by A11, A26, Def2; :: thesis:

end;

suppose v in {z} ; :: thesis:

hence ( Bottom L <= v & v <= y ) by A23, TARSKI:def 1, YELLOW_0:44; :: thesis:

end;

not z in A

proof

assume A27: z in A ; :: thesis:
not z in {y} by A10, TARSKI:def 1;
then z in B by A27, XBOOLE_0:def 5;
then z <= x by Def5;
hence contradiction by A9, ORDERS_2:7; :: thesis:

end;

then A28: card (A \/ {z}) = (card A) + 1 by CARD_2:41;
Bottom L in A by A11, Def2;
then Bottom L in A \/ {z} by XBOOLE_0:def 3;
then A \/ {z} is Chain of Bottom L,y by A22, A11, A12, A24, Def2;
then (card A) + 1 <= card A by A1, A28;
hence contradiction by NAT_1:13; :: thesis:

end;

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