let L be finite LATTICE; :: thesis: for a, b being Element of L st a < b holds
height a < height b
let a, b be Element of L; :: thesis: ( a < b implies height a < height b )
assume A1: a < b ; :: thesis: height a < height b
( ex A being Chain of Bottom L,a st height a = card A & ( for C being Chain of Bottom L,a holds card C <= height a ) ) by Def3;
then consider A being Chain of Bottom L,a such that
A2: height a = card A and
for C being Chain of Bottom L,a holds card C <= height a ;
( ex B being Chain of Bottom L,b st height b = card B & ( for D being Chain of Bottom L,b holds card D <= height b ) ) by Def3;
then consider B being Chain of Bottom L,b such that
height b = card B and
A3: for B being Chain of Bottom L,b holds card B <= height b ;
A4: Bottom L <= a by YELLOW_0:44;
A5: not b in A

proof

assume b in A ; :: thesis: contradiction
then ( Bottom L <= b & b <= a ) by A4, Def2;
hence contradiction by A1, ORDERS_2:30; :: thesis: verum

end;

set C = A \/ {b};
Bottom L in A by A4, Def2;
then A6: Bottom L in A \/ {b} by XBOOLE_0:def 3;
A7: b in A \/ {b}

proof

b in {b} by TARSKI:def 1;
hence b in A \/ {b} by XBOOLE_0:def 3; :: thesis: verum

end;

A8: for z being Element of L st z in A \/ {b} holds
( Bottom L <= z & z <= b )

proof

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

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

suppose A10: z in A ; :: thesis: ( Bottom L <= z & z <= b )

thus Bottom L <= z by YELLOW_0:44; :: thesis: z <= b
z <= a by A4, A10, Def2;
then z < b by A1, ORDERS_2:32;
hence z <= b by ORDERS_2:def 10; :: thesis: verum

end;

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

hence ( Bottom L <= z & z <= b ) by TARSKI:def 1, YELLOW_0:44; :: thesis: verum

end;

end;

end;

A11: A \/ {b} is strongly_connected Subset of L

proof

the InternalRel of L is_strongly_connected_in A \/ {b}

proof

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

proof

assume A12: ( x in A \/ {b} & y in A \/ {b} ) ; :: thesis: ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L )

per cases ( ( x in A & y in A ) or ( x in A & y in {b} ) or ( x in {b} & y in A ) or ( x in {b} & y in {b} ) ) by A12, XBOOLE_0:def 3;

suppose A13: ( x in A & y in A ) ; :: thesis: ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L )

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

end;

suppose A14: ( x in A & y in {b} ) ; :: thesis: ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L )

then A15: y = b by TARSKI:def 1;
reconsider x = x as Element of L by A14;
Bottom L <= a by YELLOW_0:44;
then x <= a by A14, Def2;
then x < b by A1, ORDERS_2:32;
then x <= b by ORDERS_2:def 10;
hence ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L ) by A15, ORDERS_2:def 9; :: thesis: verum

end;

suppose A16: ( x in {b} & y in A ) ; :: thesis: ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L )

then A17: x = b by TARSKI:def 1;
reconsider y = y as Element of L by A16;
Bottom L <= a by YELLOW_0:44;
then y <= a by A16, Def2;
then y < b by A1, ORDERS_2:32;
then y <= b by ORDERS_2:def 10;
hence ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L ) by A17, ORDERS_2:def 9; :: thesis: verum

end;

suppose A18: ( x in {b} & y in {b} ) ; :: thesis: ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L )

then reconsider x = x, y = y as Element of L ;
( x = b & y = b ) by A18, TARSKI:def 1;
then x <= y ;
hence ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L ) by ORDERS_2:def 9; :: thesis: verum

end;

end;

end;

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

end;

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

end;

Bottom L <= b by YELLOW_0:44;
then A19: A \/ {b} is Chain of Bottom L,b by A6, A7, A8, A11, Def2;
card (A \/ {b}) = (card A) + 1 by A5, CARD_2:54;
then (height a) + 1 <= height b by A2, A3, A19;
hence height a < height b by NAT_1:13; :: thesis: verum