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 )

( 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

A1: height a = card A and

for C being Chain of Bottom L,a holds card C <= height a ;

set C = A \/ {b};

b in {b} by TARSKI:def 1;

then A2: b in A \/ {b} by XBOOLE_0:def 3;

A3: Bottom L <= a by YELLOW_0:44;

then Bottom L in A by Def2;

then A4: Bottom L in A \/ {b} by XBOOLE_0:def 3;

assume A5: a < b ; :: thesis: height a < height b

not b in A

the InternalRel of L is_strongly_connected_in A \/ {b}

A15: for z being Element of L st z in A \/ {b} holds

( Bottom L <= z & z <= b )

then A \/ {b} is Chain of Bottom L,b by A4, A2, A15, A14, Def2;

then (height a) + 1 <= height b by A1, A6, Def3;

hence height a < height b by NAT_1:13; :: thesis: verum

height a < height b

let a, b be Element of L; :: thesis: ( a < b implies 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

A1: height a = card A and

for C being Chain of Bottom L,a holds card C <= height a ;

set C = A \/ {b};

b in {b} by TARSKI:def 1;

then A2: b in A \/ {b} by XBOOLE_0:def 3;

A3: Bottom L <= a by YELLOW_0:44;

then Bottom L in A by Def2;

then A4: Bottom L in A \/ {b} by XBOOLE_0:def 3;

assume A5: a < b ; :: thesis: height a < height b

not b in A

proof

then A6:
card (A \/ {b}) = (card A) + 1
by CARD_2:41;
assume
b in A
; :: thesis: contradiction

then b <= a by A3, Def2;

hence contradiction by A5, ORDERS_2:6; :: thesis: verum

end;then b <= a by A3, Def2;

hence contradiction by A5, ORDERS_2:6; :: thesis: verum

the InternalRel of L is_strongly_connected_in A \/ {b}

proof

then A14:
A \/ {b} is strongly_connected Subset of L
by ORDERS_2:def 7;
let x, y be object ; :: 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 )

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

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
assume A7:
( x in A \/ {b} & y in A \/ {b} )
; :: thesis: ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L )

end;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 A7, XBOOLE_0:def 3;

end;

suppose A8:
( 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 A8, ORDERS_2:11;

hence ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L ) by ORDERS_2:def 5; :: thesis: verum

end;( x <= y or y <= x ) by A8, ORDERS_2:11;

hence ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L ) by ORDERS_2:def 5; :: thesis: verum

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

then reconsider x = x as Element of L ;

Bottom L <= a by YELLOW_0:44;

then x <= a by A9, Def2;

then x < b by A5, ORDERS_2:7;

then A10: x <= b by ORDERS_2:def 6;

y = b by A9, TARSKI:def 1;

hence ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L ) by A10, ORDERS_2:def 5; :: thesis: verum

end;Bottom L <= a by YELLOW_0:44;

then x <= a by A9, Def2;

then x < b by A5, ORDERS_2:7;

then A10: x <= b by ORDERS_2:def 6;

y = b by A9, TARSKI:def 1;

hence ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L ) by A10, ORDERS_2:def 5; :: thesis: verum

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

then reconsider y = y as Element of L ;

Bottom L <= a by YELLOW_0:44;

then y <= a by A11, Def2;

then y < b by A5, ORDERS_2:7;

then A12: y <= b by ORDERS_2:def 6;

x = b by A11, TARSKI:def 1;

hence ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L ) by A12, ORDERS_2:def 5; :: thesis: verum

end;Bottom L <= a by YELLOW_0:44;

then y <= a by A11, Def2;

then y < b by A5, ORDERS_2:7;

then A12: y <= b by ORDERS_2:def 6;

x = b by A11, TARSKI:def 1;

hence ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L ) by A12, ORDERS_2:def 5; :: thesis: verum

suppose A13:
( 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 by A13, TARSKI:def 1;

then x <= y by A13, TARSKI:def 1;

hence ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L ) by ORDERS_2:def 5; :: thesis: verum

end;x = b by A13, TARSKI:def 1;

then x <= y by A13, TARSKI:def 1;

hence ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L ) by ORDERS_2:def 5; :: thesis: verum

A15: for z being Element of L st z in A \/ {b} holds

( Bottom L <= z & z <= b )

proof

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

assume A16: z in A \/ {b} ; :: thesis: ( Bottom L <= z & z <= b )

end;assume A16: z in A \/ {b} ; :: thesis: ( Bottom L <= z & z <= b )

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

end;

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

thus
Bottom L <= z
by YELLOW_0:44; :: thesis: z <= b

z <= a by A3, A17, Def2;

then z < b by A5, ORDERS_2:7;

hence z <= b by ORDERS_2:def 6; :: thesis: verum

end;z <= a by A3, A17, Def2;

then z < b by A5, ORDERS_2:7;

hence z <= b by ORDERS_2:def 6; :: thesis: verum

then A \/ {b} is Chain of Bottom L,b by A4, A2, A15, A14, Def2;

then (height a) + 1 <= height b by A1, A6, Def3;

hence height a < height b by NAT_1:13; :: thesis: verum