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
proof
assume b in A ; :: thesis: contradiction
then b <= a by A3, Def2;
hence contradiction by A5, ORDERS_2:6; :: thesis: verum
end;
then A6: card (A \/ {b}) = (card A) + 1 by CARD_2:41;
the InternalRel of L is_strongly_connected_in A \/ {b}
proof
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 )
proof
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 )
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;
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;
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;
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;
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;
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;
then A14: A \/ {b} is strongly_connected Subset of L by ORDERS_2:def 7;
A15: 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 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;
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;
Bottom L <= b by YELLOW_0:44;
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