let G be _finite chordal _Graph; :: thesis: for L being PartFunc of (the_Vertices_of G),NAT st L is with_property_T & dom L = the_Vertices_of G holds

for V being VertexScheme of G st V " = L holds

V is perfect

let L be PartFunc of (the_Vertices_of G),NAT; :: thesis: ( L is with_property_T & dom L = the_Vertices_of G implies for V being VertexScheme of G st V " = L holds

V is perfect )

assume that

A1: L is with_property_T and

A2: dom L = the_Vertices_of G ; :: thesis: for V being VertexScheme of G st V " = L holds

V is perfect

defpred S_{1}[ Path of G] means ( len $1 >= 5 & $1 is open & $1 is chordless & L . ($1 .first()) > L . ($1 .last()) & L . ($1 .last()) > L . ($1 . 3) & ex i being odd Element of NAT st

( 1 < i & i < len $1 & ( for j, k being odd Element of NAT st i <= j & j < k & k <= len $1 holds

L . ($1 . j) < L . ($1 . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= i holds

L . ($1 . j) > L . ($1 . k) ) ) );

let V be VertexScheme of G; :: thesis: ( V " = L implies V is perfect )

assume A3: V " = L ; :: thesis: V is perfect

A4: V is one-to-one by CHORD:def 12;

len V = card (the_Vertices_of G) by CHORD:104;

then dom V = Seg (G .order()) by FINSEQ_1:def 3;

then A5: rng L = Seg (G .order()) by A3, A4, FUNCT_1:33;

for V being VertexScheme of G st V " = L holds

V is perfect

let L be PartFunc of (the_Vertices_of G),NAT; :: thesis: ( L is with_property_T & dom L = the_Vertices_of G implies for V being VertexScheme of G st V " = L holds

V is perfect )

assume that

A1: L is with_property_T and

A2: dom L = the_Vertices_of G ; :: thesis: for V being VertexScheme of G st V " = L holds

V is perfect

defpred S

( 1 < i & i < len $1 & ( for j, k being odd Element of NAT st i <= j & j < k & k <= len $1 holds

L . ($1 . j) < L . ($1 . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= i holds

L . ($1 . j) > L . ($1 . k) ) ) );

let V be VertexScheme of G; :: thesis: ( V " = L implies V is perfect )

assume A3: V " = L ; :: thesis: V is perfect

A4: V is one-to-one by CHORD:def 12;

len V = card (the_Vertices_of G) by CHORD:104;

then dom V = Seg (G .order()) by FINSEQ_1:def 3;

then A5: rng L = Seg (G .order()) by A3, A4, FUNCT_1:33;

A6: now :: thesis: for R being Path of G holds not S_{1}[R]

A131:
L " = V
by A3, A4, FUNCT_1:43;defpred S_{2}[ Nat] means ex P being Path of G st

( S_{1}[P] & L . (P .last()) = $1 );

A7: for k being Nat st S_{2}[k] holds

k <= G .order()_{1}[R]

assume S_{1}[R]
; :: thesis: contradiction

then A9: ex k being Nat st S_{2}[k]
;

consider k being Nat such that

A10: S_{2}[k]
and

A11: for n being Nat st S_{2}[n] holds

n <= k from NAT_1:sch 6(A7, A9);

consider P being Path of G such that

A12: S_{1}[P]
and

A13: L . (P .last()) = k by A10;

3 <= len P by A12, XXREAL_0:2;

then P . 3 = P .vertexAt ((2 * 1) + 1) by GLIB_001:def 8;

then reconsider a = P . 3 as Vertex of G ;

A14: 3 < len P by A12, XXREAL_0:2;

reconsider b = P .last() as Vertex of G ;

reconsider c = P .first() as Vertex of G ;

(2 * 0) + 1 < (2 * 1) + 1 ;

then ex ez being object st ez Joins P . 1,P . 3,G by A12, A14, CHORD:92;

then c,a are_adjacent by CHORD:def 3;

then consider d being Vertex of G such that

d in dom L and

A18: L . b < L . d and

A19: b,d are_adjacent and

A20: not a,d are_adjacent by A1, A2, A12, A17;

A21: L . d <> L . c by A2, A3, A4, A17, A19, FUNCT_1:def 4;

consider i being odd Element of NAT such that

A22: 1 < i and

i < len P and

A23: for j, k being odd Element of NAT st i <= j & j < k & k <= len P holds

L . (P . j) < L . (P . k) and

A24: for j, k being odd Element of NAT st 1 <= j & j < k & k <= i holds

L . (P . j) > L . (P . k) by A12;

A25: L . a < L . d by A12, A18, XXREAL_0:2;

_{3}[ Nat] means ( $1 is odd & 3 < $1 & $1 <= len P & ex e being object st e Joins P . $1,d,G );

ex el being object st el Joins P .last() ,d,G by A19, CHORD:def 3;

then A32: ex k being Nat st S_{3}[k]
by A14;

ex j being Nat st

( S_{3}[j] & ( for n being Nat st S_{3}[n] holds

j <= n ) ) from NAT_1:sch 5(A32);

then consider j being Nat such that

A33: j is odd and

A34: 3 < j and

A35: j <= len P and

A36: ex e being object st e Joins P . j,d,G and

A37: for i being Nat st S_{3}[i] holds

j <= i ;

reconsider j = j as odd Element of NAT by A33, ORDINAL1:def 12;

reconsider C = P .cut (1,j) as Path of G ;

consider e being object such that

A38: e Joins P . j,d,G by A36;

(2 * 0) + 1 < j by A34, XXREAL_0:2;

then A39: ( C is open & C is chordless ) by A12, A35, CHORD:93;

A40: (2 * 0) + 1 <= j by CHORD:2;

then A41: (len C) + 1 = j + 1 by A35, GLIB_001:36;

then A44: C . 3 = a by A42;

C .vertices() c= P .vertices() by A35, A40, GLIB_001:94;

then A52: not d in C .vertices() by A26;

then reconsider D = C .addEdge e as Path of G by A51, A39, A45, CHORD:97;

reconsider R = D .reverse() as Path of G ;

A53: C .last() = P . j by A35, A40, GLIB_001:37;

then A54: len D = (len C) + 2 by A38, GLIB_001:64;

then A58: D .first() = c by A38, A53, GLIB_001:63;

then A59: R .last() = c by GLIB_001:22;

3 in dom C by A34, A41, FINSEQ_3:25;

then A60: D . 3 = a by A38, A53, A44, GLIB_001:65;

A61: D is chordless by A52, A51, A39, A45, CHORD:97;

A62: D .last() = d by A38, A53, GLIB_001:63;

then A63: R .first() = d by GLIB_001:22;

A64: for n being odd Element of NAT st n <= len R holds

( R . n = D . (((len D) - n) + 1) & ((len D) - n) + 1 is Element of NAT )

( 1 < i & i < len D & ( for j, k being odd Element of NAT st i <= j & j < k & k <= len D holds

L . (D . j) < L . (D . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= i holds

L . (D . j) > L . (D . k) ) )

( 1 < i & i < len R & ( for j, k being odd Element of NAT st i <= j & j < k & k <= len R holds

L . (R . j) < L . (R . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= i holds

L . (R . j) > L . (R . k) ) )

then A127: len R >= 3 + 2 by GLIB_001:21;

then 3 <= len R by XXREAL_0:2;

then 3 in dom R by FINSEQ_3:25;

then R . 3 = D . (((len D) - 3) + 1) by GLIB_001:25;

then R . 3 = C . j by A41, A54, A67;

then A128: L . (R .last()) > L . (R . 3) by A42, A59, A55;

d <> c by A15, A19, CHORD:def 3;

then A129: R is open by A63, A59;

D is open by A52, A51, A39, A45, CHORD:97;

then L . c <= L . d by A11, A13, A18, A25, A61, A126, A58, A62, A60, A69;

then A130: L . c < L . d by A21, XXREAL_0:1;

R is chordless by A61, CHORD:91;

hence contradiction by A11, A12, A13, A130, A63, A59, A129, A127, A128, A101; :: thesis: verum

end;( S

A7: for k being Nat st S

k <= G .order()

proof

let R be Path of G; :: thesis: not S
let k be Nat; :: thesis: ( S_{2}[k] implies k <= G .order() )

assume S_{2}[k]
; :: thesis: k <= G .order()

then consider P being Path of G such that

S_{1}[P]
and

A8: L . (P .last()) = k ;

L . (P .last()) in Seg (G .order()) by A2, A5, FUNCT_1:def 3;

hence k <= G .order() by A8, FINSEQ_1:1; :: thesis: verum

end;assume S

then consider P being Path of G such that

S

A8: L . (P .last()) = k ;

L . (P .last()) in Seg (G .order()) by A2, A5, FUNCT_1:def 3;

hence k <= G .order() by A8, FINSEQ_1:1; :: thesis: verum

assume S

then A9: ex k being Nat st S

consider k being Nat such that

A10: S

A11: for n being Nat st S

n <= k from NAT_1:sch 6(A7, A9);

consider P being Path of G such that

A12: S

A13: L . (P .last()) = k by A10;

3 <= len P by A12, XXREAL_0:2;

then P . 3 = P .vertexAt ((2 * 1) + 1) by GLIB_001:def 8;

then reconsider a = P . 3 as Vertex of G ;

A14: 3 < len P by A12, XXREAL_0:2;

reconsider b = P .last() as Vertex of G ;

reconsider c = P .first() as Vertex of G ;

A15: now :: thesis: for e being object holds not e Joins c,b,G

then A17:
not b,c are_adjacent
by CHORD:def 3;
(2 * 0) + 1 < len P
by A12, XXREAL_0:2;

then A16: ( ex e being object st e Joins P . 1,P . (len P),G iff 1 + 2 = len P ) by A12, CHORD:92;

let e be object ; :: thesis: not e Joins c,b,G

assume e Joins c,b,G ; :: thesis: contradiction

hence contradiction by A12, A16; :: thesis: verum

end;then A16: ( ex e being object st e Joins P . 1,P . (len P),G iff 1 + 2 = len P ) by A12, CHORD:92;

let e be object ; :: thesis: not e Joins c,b,G

assume e Joins c,b,G ; :: thesis: contradiction

hence contradiction by A12, A16; :: thesis: verum

(2 * 0) + 1 < (2 * 1) + 1 ;

then ex ez being object st ez Joins P . 1,P . 3,G by A12, A14, CHORD:92;

then c,a are_adjacent by CHORD:def 3;

then consider d being Vertex of G such that

d in dom L and

A18: L . b < L . d and

A19: b,d are_adjacent and

A20: not a,d are_adjacent by A1, A2, A12, A17;

A21: L . d <> L . c by A2, A3, A4, A17, A19, FUNCT_1:def 4;

consider i being odd Element of NAT such that

A22: 1 < i and

i < len P and

A23: for j, k being odd Element of NAT st i <= j & j < k & k <= len P holds

L . (P . j) < L . (P . k) and

A24: for j, k being odd Element of NAT st 1 <= j & j < k & k <= i holds

L . (P . j) > L . (P . k) by A12;

A25: L . a < L . d by A12, A18, XXREAL_0:2;

A26: now :: thesis: not d in P .vertices()

defpred Sassume
d in P .vertices()
; :: thesis: contradiction

then consider dn being odd Element of NAT such that

A27: dn <= len P and

A28: P . dn = d by GLIB_001:87;

A29: 1 <= dn by CHORD:2;

dn <> 1 by A15, A19, A28, CHORD:def 3;

then (2 * 0) + 1 < dn by A29, XXREAL_0:1;

then 1 + 2 <= dn by CHORD:4;

then A30: (2 * 1) + 1 < dn by A12, A18, A28, XXREAL_0:1;

A31: dn < len P by A18, A27, A28, XXREAL_0:1;

end;then consider dn being odd Element of NAT such that

A27: dn <= len P and

A28: P . dn = d by GLIB_001:87;

A29: 1 <= dn by CHORD:2;

dn <> 1 by A15, A19, A28, CHORD:def 3;

then (2 * 0) + 1 < dn by A29, XXREAL_0:1;

then 1 + 2 <= dn by CHORD:4;

then A30: (2 * 1) + 1 < dn by A12, A18, A28, XXREAL_0:1;

A31: dn < len P by A18, A27, A28, XXREAL_0:1;

ex el being object st el Joins P .last() ,d,G by A19, CHORD:def 3;

then A32: ex k being Nat st S

ex j being Nat st

( S

j <= n ) ) from NAT_1:sch 5(A32);

then consider j being Nat such that

A33: j is odd and

A34: 3 < j and

A35: j <= len P and

A36: ex e being object st e Joins P . j,d,G and

A37: for i being Nat st S

j <= i ;

reconsider j = j as odd Element of NAT by A33, ORDINAL1:def 12;

reconsider C = P .cut (1,j) as Path of G ;

consider e being object such that

A38: e Joins P . j,d,G by A36;

(2 * 0) + 1 < j by A34, XXREAL_0:2;

then A39: ( C is open & C is chordless ) by A12, A35, CHORD:93;

A40: (2 * 0) + 1 <= j by CHORD:2;

then A41: (len C) + 1 = j + 1 by A35, GLIB_001:36;

A42: now :: thesis: for n being odd Element of NAT st n <= j holds

C . n = P . n

(2 * 1) + 1 < j
by A34;C . n = P . n

let n be odd Element of NAT ; :: thesis: ( n <= j implies C . n = P . n )

assume A43: n <= j ; :: thesis: C . n = P . n

1 <= n by CHORD:2;

then n in dom C by A41, A43, FINSEQ_3:25;

then C . n = P . ((1 + n) - 1) by A35, A40, GLIB_001:47;

hence C . n = P . n ; :: thesis: verum

end;assume A43: n <= j ; :: thesis: C . n = P . n

1 <= n by CHORD:2;

then n in dom C by A41, A43, FINSEQ_3:25;

then C . n = P . ((1 + n) - 1) by A35, A40, GLIB_001:47;

hence C . n = P . n ; :: thesis: verum

then A44: C . 3 = a by A42;

A45: now :: thesis: for f being object holds not f Joins C . ((len C) - 2),d,G

A51:
e Joins C .last() ,d,G
by A35, A38, A40, GLIB_001:37;
len C > (2 * 1) + 1
by A34, A41;

then A46: len C >= 3 + 2 by CHORD:4;

let f be object ; :: thesis: not f Joins C . ((len C) - 2),d,G

assume A47: f Joins C . ((len C) - 2),d,G ; :: thesis: contradiction

len C <> 5 by A20, A44, A47, CHORD:def 3;

then len C > 5 by A46, XXREAL_0:1;

then A48: (3 + 2) - 2 < (len C) - 2 by XREAL_1:9;

then 0 < (len C) - (2 * 1) ;

then reconsider cc = (len C) - 2 as odd Element of NAT by INT_1:3;

A49: cc < len C by XREAL_1:44;

then A50: cc < len P by A35, A41, XXREAL_0:2;

f Joins P . cc,d,G by A41, A42, A47, A49;

hence contradiction by A37, A41, A48, A49, A50; :: thesis: verum

end;then A46: len C >= 3 + 2 by CHORD:4;

let f be object ; :: thesis: not f Joins C . ((len C) - 2),d,G

assume A47: f Joins C . ((len C) - 2),d,G ; :: thesis: contradiction

len C <> 5 by A20, A44, A47, CHORD:def 3;

then len C > 5 by A46, XXREAL_0:1;

then A48: (3 + 2) - 2 < (len C) - 2 by XREAL_1:9;

then 0 < (len C) - (2 * 1) ;

then reconsider cc = (len C) - 2 as odd Element of NAT by INT_1:3;

A49: cc < len C by XREAL_1:44;

then A50: cc < len P by A35, A41, XXREAL_0:2;

f Joins P . cc,d,G by A41, A42, A47, A49;

hence contradiction by A37, A41, A48, A49, A50; :: thesis: verum

C .vertices() c= P .vertices() by A35, A40, GLIB_001:94;

then A52: not d in C .vertices() by A26;

then reconsider D = C .addEdge e as Path of G by A51, A39, A45, CHORD:97;

reconsider R = D .reverse() as Path of G ;

A53: C .last() = P . j by A35, A40, GLIB_001:37;

then A54: len D = (len C) + 2 by A38, GLIB_001:64;

A55: now :: thesis: L . (P . j) < L . c

C .first() = P .first()
by A35, A40, GLIB_001:37;end;

then A58: D .first() = c by A38, A53, GLIB_001:63;

then A59: R .last() = c by GLIB_001:22;

3 in dom C by A34, A41, FINSEQ_3:25;

then A60: D . 3 = a by A38, A53, A44, GLIB_001:65;

A61: D is chordless by A52, A51, A39, A45, CHORD:97;

A62: D .last() = d by A38, A53, GLIB_001:63;

then A63: R .first() = d by GLIB_001:22;

A64: for n being odd Element of NAT st n <= len R holds

( R . n = D . (((len D) - n) + 1) & ((len D) - n) + 1 is Element of NAT )

proof

let n be odd Element of NAT ; :: thesis: ( n <= len R implies ( R . n = D . (((len D) - n) + 1) & ((len D) - n) + 1 is Element of NAT ) )

assume A65: n <= len R ; :: thesis: ( R . n = D . (((len D) - n) + 1) & ((len D) - n) + 1 is Element of NAT )

1 <= n by CHORD:2;

then A66: n in dom R by A65, FINSEQ_3:25;

hence R . n = D . (((len D) - n) + 1) by GLIB_001:25; :: thesis: ((len D) - n) + 1 is Element of NAT

((len D) - n) + 1 in dom D by A66, GLIB_001:25;

hence ((len D) - n) + 1 is Element of NAT ; :: thesis: verum

end;assume A65: n <= len R ; :: thesis: ( R . n = D . (((len D) - n) + 1) & ((len D) - n) + 1 is Element of NAT )

1 <= n by CHORD:2;

then A66: n in dom R by A65, FINSEQ_3:25;

hence R . n = D . (((len D) - n) + 1) by GLIB_001:25; :: thesis: ((len D) - n) + 1 is Element of NAT

((len D) - n) + 1 in dom D by A66, GLIB_001:25;

hence ((len D) - n) + 1 is Element of NAT ; :: thesis: verum

A67: now :: thesis: for n being odd Nat st n <= j holds

C . n = D . n

A69:
ex i being odd Element of NAT st C . n = D . n

let n be odd Nat; :: thesis: ( n <= j implies C . n = D . n )

assume A68: n <= j ; :: thesis: C . n = D . n

1 <= n by CHORD:2;

then n in dom C by A41, A68, FINSEQ_3:25;

hence C . n = D . n by A51, GLIB_001:65; :: thesis: verum

end;assume A68: n <= j ; :: thesis: C . n = D . n

1 <= n by CHORD:2;

then n in dom C by A41, A68, FINSEQ_3:25;

hence C . n = D . n by A51, GLIB_001:65; :: thesis: verum

( 1 < i & i < len D & ( for j, k being odd Element of NAT st i <= j & j < k & k <= len D holds

L . (D . j) < L . (D . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= i holds

L . (D . j) > L . (D . k) ) )

proof
end;

A101:
ex i being odd Element of NAT st per cases
( j <= i or i < j )
;

end;

suppose A70:
j <= i
; :: thesis: ex i being odd Element of NAT st

( 1 < i & i < len D & ( for j, k being odd Element of NAT st i <= j & j < k & k <= len D holds

L . (D . j) < L . (D . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= i holds

L . (D . j) > L . (D . k) ) )

L . (D . j) < L . (D . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= j holds

L . (D . j) > L . (D . k) ) )

L . (D . j) < L . (D . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= j holds

L . (D . j) > L . (D . k) ) ) by A34, A41, A54, A71, XREAL_1:29, XXREAL_0:2; :: thesis: verum

end;

( 1 < i & i < len D & ( for j, k being odd Element of NAT st i <= j & j < k & k <= len D holds

L . (D . j) < L . (D . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= i holds

L . (D . j) > L . (D . k) ) )

A71: now :: thesis: for e, f being odd Element of NAT st j <= e & e < f & f <= len D holds

L . (D . e) < L . (D . f)

take
j
; :: thesis: ( 1 < j & j < len D & ( for j, k being odd Element of NAT st j <= j & j < k & k <= len D holds L . (D . e) < L . (D . f)

1 < (2 * 1) + 1
;

then A72: L . (P . 3) > L . (P . j) by A24, A34, A70;

let e, f be odd Element of NAT ; :: thesis: ( j <= e & e < f & f <= len D implies L . (D . e) < L . (D . f) )

assume that

A73: j <= e and

A74: e < f and

A75: f <= len D ; :: thesis: L . (D . e) < L . (D . f)

e < j + (2 * 1) by A41, A54, A74, A75, XXREAL_0:2;

then e <= (j + 2) - 2 by CHORD:3;

then A76: e = j by A73, XXREAL_0:1;

then D . e = C . j by A67;

then A77: D . e = P . j by A42;

(len C) + 2 <= f by A41, A74, A76, CHORD:4;

then D . f = d by A54, A62, A75, XXREAL_0:1;

hence L . (D . e) < L . (D . f) by A25, A77, A72, XXREAL_0:2; :: thesis: verum

end;then A72: L . (P . 3) > L . (P . j) by A24, A34, A70;

let e, f be odd Element of NAT ; :: thesis: ( j <= e & e < f & f <= len D implies L . (D . e) < L . (D . f) )

assume that

A73: j <= e and

A74: e < f and

A75: f <= len D ; :: thesis: L . (D . e) < L . (D . f)

e < j + (2 * 1) by A41, A54, A74, A75, XXREAL_0:2;

then e <= (j + 2) - 2 by CHORD:3;

then A76: e = j by A73, XXREAL_0:1;

then D . e = C . j by A67;

then A77: D . e = P . j by A42;

(len C) + 2 <= f by A41, A74, A76, CHORD:4;

then D . f = d by A54, A62, A75, XXREAL_0:1;

hence L . (D . e) < L . (D . f) by A25, A77, A72, XXREAL_0:2; :: thesis: verum

L . (D . j) < L . (D . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= j holds

L . (D . j) > L . (D . k) ) )

now :: thesis: for e, f being odd Element of NAT st 1 <= e & e < f & f <= j holds

L . (D . e) > L . (D . f)

hence
( 1 < j & j < len D & ( for j, k being odd Element of NAT st j <= j & j < k & k <= len D holds L . (D . e) > L . (D . f)

let e, f be odd Element of NAT ; :: thesis: ( 1 <= e & e < f & f <= j implies L . (D . e) > L . (D . f) )

assume that

A78: 1 <= e and

A79: e < f and

A80: f <= j ; :: thesis: L . (D . e) > L . (D . f)

D . e = C . e by A67, A79, A80, XXREAL_0:2;

then A81: D . e = P . e by A42, A79, A80, XXREAL_0:2;

D . f = C . f by A67, A80;

then A82: D . f = P . f by A42, A80;

f <= i by A70, A80, XXREAL_0:2;

hence L . (D . e) > L . (D . f) by A24, A78, A79, A81, A82; :: thesis: verum

end;assume that

A78: 1 <= e and

A79: e < f and

A80: f <= j ; :: thesis: L . (D . e) > L . (D . f)

D . e = C . e by A67, A79, A80, XXREAL_0:2;

then A81: D . e = P . e by A42, A79, A80, XXREAL_0:2;

D . f = C . f by A67, A80;

then A82: D . f = P . f by A42, A80;

f <= i by A70, A80, XXREAL_0:2;

hence L . (D . e) > L . (D . f) by A24, A78, A79, A81, A82; :: thesis: verum

L . (D . j) < L . (D . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= j holds

L . (D . j) > L . (D . k) ) ) by A34, A41, A54, A71, XREAL_1:29, XXREAL_0:2; :: thesis: verum

suppose A83:
i < j
; :: thesis: ex i being odd Element of NAT st

( 1 < i & i < len D & ( for j, k being odd Element of NAT st i <= j & j < k & k <= len D holds

L . (D . j) < L . (D . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= i holds

L . (D . j) > L . (D . k) ) )

( 1 < i & i < len D & ( for j, k being odd Element of NAT st i <= j & j < k & k <= len D holds

L . (D . j) < L . (D . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= i holds

L . (D . j) > L . (D . k) ) )

take
i
; :: thesis: ( 1 < i & i < len D & ( for j, k being odd Element of NAT st i <= j & j < k & k <= len D holds

L . (D . j) < L . (D . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= i holds

L . (D . j) > L . (D . k) ) )

hence ( 1 < i & i < len D & ( for j, k being odd Element of NAT st i <= j & j < k & k <= len D holds

L . (D . j) < L . (D . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= i holds

L . (D . j) > L . (D . k) ) ) by A22, A83, A84, A95, XXREAL_0:2; :: thesis: verum

end;L . (D . j) < L . (D . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= i holds

L . (D . j) > L . (D . k) ) )

A84: now :: thesis: for e, f being odd Element of NAT st i <= e & e < f & f <= len D holds

L . (D . e) < L . (D . f)

L . (D . e) < L . (D . f)

let e, f be odd Element of NAT ; :: thesis: ( i <= e & e < f & f <= len D implies L . (D . b_{1}) < L . (D . b_{2}) )

assume that

A85: i <= e and

A86: e < f and

A87: f <= len D ; :: thesis: L . (D . b_{1}) < L . (D . b_{2})

e < j + (2 * 1) by A41, A54, A86, A87, XXREAL_0:2;

then A88: e <= (j + 2) - 2 by CHORD:3;

then A89: e <= len P by A35, XXREAL_0:2;

A90: D . e = C . e by A67, A88;

then A91: D . e = P . e by A42, A88;

end;assume that

A85: i <= e and

A86: e < f and

A87: f <= len D ; :: thesis: L . (D . b

e < j + (2 * 1) by A41, A54, A86, A87, XXREAL_0:2;

then A88: e <= (j + 2) - 2 by CHORD:3;

then A89: e <= len P by A35, XXREAL_0:2;

A90: D . e = C . e by A67, A88;

then A91: D . e = P . e by A42, A88;

A95: now :: thesis: for e, f being odd Element of NAT st 1 <= e & e < f & f <= i holds

L . (D . e) > L . (D . f)

len D > j
by A41, A54, XREAL_1:29;L . (D . e) > L . (D . f)

let e, f be odd Element of NAT ; :: thesis: ( 1 <= e & e < f & f <= i implies L . (D . e) > L . (D . f) )

assume that

A96: 1 <= e and

A97: e < f and

A98: f <= i ; :: thesis: L . (D . e) > L . (D . f)

D . f = C . f by A67, A83, A98, XXREAL_0:2;

then A99: D . f = P . f by A42, A83, A98, XXREAL_0:2;

A100: e <= i by A97, A98, XXREAL_0:2;

then D . e = C . e by A67, A83, XXREAL_0:2;

then D . e = P . e by A42, A83, A100, XXREAL_0:2;

hence L . (D . e) > L . (D . f) by A24, A96, A97, A98, A99; :: thesis: verum

end;assume that

A96: 1 <= e and

A97: e < f and

A98: f <= i ; :: thesis: L . (D . e) > L . (D . f)

D . f = C . f by A67, A83, A98, XXREAL_0:2;

then A99: D . f = P . f by A42, A83, A98, XXREAL_0:2;

A100: e <= i by A97, A98, XXREAL_0:2;

then D . e = C . e by A67, A83, XXREAL_0:2;

then D . e = P . e by A42, A83, A100, XXREAL_0:2;

hence L . (D . e) > L . (D . f) by A24, A96, A97, A98, A99; :: thesis: verum

hence ( 1 < i & i < len D & ( for j, k being odd Element of NAT st i <= j & j < k & k <= len D holds

L . (D . j) < L . (D . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= i holds

L . (D . j) > L . (D . k) ) ) by A22, A83, A84, A95, XXREAL_0:2; :: thesis: verum

( 1 < i & i < len R & ( for j, k being odd Element of NAT st i <= j & j < k & k <= len R holds

L . (R . j) < L . (R . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= i holds

L . (R . j) > L . (R . k) ) )

proof

A126:
len D >= 3 + 2
by A34, A41, A54, XREAL_1:7;
consider i being odd Element of NAT such that

A102: 1 < i and

A103: i < len D and

A104: for j, k being odd Element of NAT st i <= j & j < k & k <= len D holds

L . (D . j) < L . (D . k) and

A105: for j, k being odd Element of NAT st 1 <= j & j < k & k <= i holds

L . (D . j) > L . (D . k) by A69;

set ir = ((len D) - i) + 1;

(len D) - 1 > (len D) - i by A102, XREAL_1:15;

then A106: ((len D) - 1) + 1 > ((len D) - i) + 1 by XREAL_1:8;

then A107: ((len D) - i) + 1 < len R by GLIB_001:21;

A108: (len D) - (len D) < (len D) - i by A103, XREAL_1:15;

then reconsider ir = ((len D) - i) + 1 as odd Element of NAT by INT_1:3;

L . (R . j) < L . (R . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= ir holds

L . (R . j) > L . (R . k) ) )

hence ( 1 < ir & ir < len R & ( for j, k being odd Element of NAT st ir <= j & j < k & k <= len R holds

L . (R . j) < L . (R . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= ir holds

L . (R . j) > L . (R . k) ) ) by A106, A118, A109, GLIB_001:21; :: thesis: verum

end;A102: 1 < i and

A103: i < len D and

A104: for j, k being odd Element of NAT st i <= j & j < k & k <= len D holds

L . (D . j) < L . (D . k) and

A105: for j, k being odd Element of NAT st 1 <= j & j < k & k <= i holds

L . (D . j) > L . (D . k) by A69;

set ir = ((len D) - i) + 1;

(len D) - 1 > (len D) - i by A102, XREAL_1:15;

then A106: ((len D) - 1) + 1 > ((len D) - i) + 1 by XREAL_1:8;

then A107: ((len D) - i) + 1 < len R by GLIB_001:21;

A108: (len D) - (len D) < (len D) - i by A103, XREAL_1:15;

then reconsider ir = ((len D) - i) + 1 as odd Element of NAT by INT_1:3;

A109: now :: thesis: for ja, k being odd Element of NAT st 1 <= ja & ja < k & k <= ir holds

L . (R . ja) > L . (R . k)

take
ir
; :: thesis: ( 1 < ir & ir < len R & ( for j, k being odd Element of NAT st ir <= j & j < k & k <= len R holds L . (R . ja) > L . (R . k)

let ja, k be odd Element of NAT ; :: thesis: ( 1 <= ja & ja < k & k <= ir implies L . (R . ja) > L . (R . k) )

assume that

A110: 1 <= ja and

A111: ja < k and

A112: k <= ir ; :: thesis: L . (R . ja) > L . (R . k)

set jr = ((len D) - ja) + 1;

A113: k <= len R by A107, A112, XXREAL_0:2;

then A114: ja <= len R by A111, XXREAL_0:2;

then A115: R . ja = D . (((len D) - ja) + 1) by A64;

i + k <= (((len D) - i) + 1) + i by A112, XREAL_1:7;

then A116: (i + k) - k <= ((len D) + 1) - k by XREAL_1:9;

set kr = ((len D) - k) + 1;

A117: ((len D) - k) + 1 < ((len D) - ja) + 1 by A111, Lm3;

reconsider jr = ((len D) - ja) + 1 as odd Element of NAT by A64, A114;

reconsider kr = ((len D) - k) + 1 as odd Element of NAT by A64, A113;

(len D) - ja <= (len D) - 1 by A110, XREAL_1:10;

then jr <= ((len D) - 1) + 1 by XREAL_1:7;

then L . (D . kr) < L . (D . jr) by A104, A116, A117;

hence L . (R . ja) > L . (R . k) by A64, A113, A115; :: thesis: verum

end;assume that

A110: 1 <= ja and

A111: ja < k and

A112: k <= ir ; :: thesis: L . (R . ja) > L . (R . k)

set jr = ((len D) - ja) + 1;

A113: k <= len R by A107, A112, XXREAL_0:2;

then A114: ja <= len R by A111, XXREAL_0:2;

then A115: R . ja = D . (((len D) - ja) + 1) by A64;

i + k <= (((len D) - i) + 1) + i by A112, XREAL_1:7;

then A116: (i + k) - k <= ((len D) + 1) - k by XREAL_1:9;

set kr = ((len D) - k) + 1;

A117: ((len D) - k) + 1 < ((len D) - ja) + 1 by A111, Lm3;

reconsider jr = ((len D) - ja) + 1 as odd Element of NAT by A64, A114;

reconsider kr = ((len D) - k) + 1 as odd Element of NAT by A64, A113;

(len D) - ja <= (len D) - 1 by A110, XREAL_1:10;

then jr <= ((len D) - 1) + 1 by XREAL_1:7;

then L . (D . kr) < L . (D . jr) by A104, A116, A117;

hence L . (R . ja) > L . (R . k) by A64, A113, A115; :: thesis: verum

L . (R . j) < L . (R . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= ir holds

L . (R . j) > L . (R . k) ) )

A118: now :: thesis: for j, k being odd Element of NAT st ir <= j & j < k & k <= len R holds

L . (R . j) < L . (R . k)

0 + 1 < ((len D) - i) + 1
by A108, XREAL_1:8;L . (R . j) < L . (R . k)

let j, k be odd Element of NAT ; :: thesis: ( ir <= j & j < k & k <= len R implies L . (R . j) < L . (R . k) )

assume that

A119: ir <= j and

A120: j < k and

A121: k <= len R ; :: thesis: L . (R . j) < L . (R . k)

set kr = ((len D) - k) + 1;

A122: R . k = D . (((len D) - k) + 1) by A64, A121;

set jr = ((len D) - j) + 1;

A123: j <= len R by A120, A121, XXREAL_0:2;

then A124: R . j = D . (((len D) - j) + 1) by A64;

reconsider kr = ((len D) - k) + 1 as odd Element of NAT by A64, A121;

i + j >= (((len D) - i) + 1) + i by A119, XREAL_1:7;

then A125: (i + j) - j >= ((len D) + 1) - j by XREAL_1:9;

reconsider jr = ((len D) - j) + 1 as odd Element of NAT by A64, A123;

kr < jr by A120, Lm3;

hence L . (R . j) < L . (R . k) by A105, A124, A122, A125, CHORD:2; :: thesis: verum

end;assume that

A119: ir <= j and

A120: j < k and

A121: k <= len R ; :: thesis: L . (R . j) < L . (R . k)

set kr = ((len D) - k) + 1;

A122: R . k = D . (((len D) - k) + 1) by A64, A121;

set jr = ((len D) - j) + 1;

A123: j <= len R by A120, A121, XXREAL_0:2;

then A124: R . j = D . (((len D) - j) + 1) by A64;

reconsider kr = ((len D) - k) + 1 as odd Element of NAT by A64, A121;

i + j >= (((len D) - i) + 1) + i by A119, XREAL_1:7;

then A125: (i + j) - j >= ((len D) + 1) - j by XREAL_1:9;

reconsider jr = ((len D) - j) + 1 as odd Element of NAT by A64, A123;

kr < jr by A120, Lm3;

hence L . (R . j) < L . (R . k) by A105, A124, A122, A125, CHORD:2; :: thesis: verum

hence ( 1 < ir & ir < len R & ( for j, k being odd Element of NAT st ir <= j & j < k & k <= len R holds

L . (R . j) < L . (R . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= ir holds

L . (R . j) > L . (R . k) ) ) by A106, A118, A109, GLIB_001:21; :: thesis: verum

then A127: len R >= 3 + 2 by GLIB_001:21;

then 3 <= len R by XXREAL_0:2;

then 3 in dom R by FINSEQ_3:25;

then R . 3 = D . (((len D) - 3) + 1) by GLIB_001:25;

then R . 3 = C . j by A41, A54, A67;

then A128: L . (R .last()) > L . (R . 3) by A42, A59, A55;

d <> c by A15, A19, CHORD:def 3;

then A129: R is open by A63, A59;

D is open by A52, A51, A39, A45, CHORD:97;

then L . c <= L . d by A11, A13, A18, A25, A61, A126, A58, A62, A60, A69;

then A130: L . c < L . d by A21, XXREAL_0:1;

R is chordless by A61, CHORD:91;

hence contradiction by A11, A12, A13, A130, A63, A59, A129, A127, A128, A101; :: thesis: verum

now :: thesis: for a, b, c being Vertex of G st b <> c & a,b are_adjacent & a,c are_adjacent holds

for va, vb, vc being Nat st va in dom V & vb in dom V & vc in dom V & V . va = a & V . vb = b & V . vc = c & va < vb & va < vc holds

b,c are_adjacent

hence
V is perfect
by CHORD:109; :: thesis: verumfor va, vb, vc being Nat st va in dom V & vb in dom V & vc in dom V & V . va = a & V . vb = b & V . vc = c & va < vb & va < vc holds

b,c are_adjacent

let a, b, c be Vertex of G; :: thesis: ( b <> c & a,b are_adjacent & a,c are_adjacent implies for va, vb, vc being Nat st va in dom V & vb in dom V & vc in dom V & V . va = a & V . vb = b & V . vc = c & va < vb & va < vc holds

b,c are_adjacent )

assume that

A132: b <> c and

A133: a,b are_adjacent and

A134: a,c are_adjacent ; :: thesis: for va, vb, vc being Nat st va in dom V & vb in dom V & vc in dom V & V . va = a & V . vb = b & V . vc = c & va < vb & va < vc holds

b,c are_adjacent

let va, vb, vc be Nat; :: thesis: ( va in dom V & vb in dom V & vc in dom V & V . va = a & V . vb = b & V . vc = c & va < vb & va < vc implies b,c are_adjacent )

assume that

A135: va in dom V and

A136: vb in dom V and

A137: vc in dom V and

A138: V . va = a and

A139: V . vb = b and

A140: V . vc = c and

A141: va < vb and

A142: va < vc ; :: thesis: b,c are_adjacent

A143: L . a = va by A3, A4, A135, A138, FUNCT_1:34;

A144: c = V . (L . c) by A2, A3, A4, A131, FUNCT_1:34;

A145: b = V . (L . b) by A2, A3, A4, A131, FUNCT_1:34;

assume A146: not b,c are_adjacent ; :: thesis: contradiction

A147: L . b = vb by A3, A4, A136, A139, FUNCT_1:34;

A148: L . c = vc by A3, A4, A137, A140, FUNCT_1:34;

end;b,c are_adjacent )

assume that

A132: b <> c and

A133: a,b are_adjacent and

A134: a,c are_adjacent ; :: thesis: for va, vb, vc being Nat st va in dom V & vb in dom V & vc in dom V & V . va = a & V . vb = b & V . vc = c & va < vb & va < vc holds

b,c are_adjacent

let va, vb, vc be Nat; :: thesis: ( va in dom V & vb in dom V & vc in dom V & V . va = a & V . vb = b & V . vc = c & va < vb & va < vc implies b,c are_adjacent )

assume that

A135: va in dom V and

A136: vb in dom V and

A137: vc in dom V and

A138: V . va = a and

A139: V . vb = b and

A140: V . vc = c and

A141: va < vb and

A142: va < vc ; :: thesis: b,c are_adjacent

A143: L . a = va by A3, A4, A135, A138, FUNCT_1:34;

A144: c = V . (L . c) by A2, A3, A4, A131, FUNCT_1:34;

A145: b = V . (L . b) by A2, A3, A4, A131, FUNCT_1:34;

assume A146: not b,c are_adjacent ; :: thesis: contradiction

A147: L . b = vb by A3, A4, A136, A139, FUNCT_1:34;

A148: L . c = vc by A3, A4, A137, A140, FUNCT_1:34;

per cases
( L . b < L . c or L . c < L . b )
by A132, A145, A144, XXREAL_0:1;

end;

suppose A149:
L . b < L . c
; :: thesis: contradiction

A150:
(2 * 1) + 1 is odd
;

consider P being Path of G, e1, e2 being object such that

A151: P is open and

A152: len P = 5 and

P .length() = 2 and

e1 Joins c,a,G and

e2 Joins a,b,G and

P .edges() = {e1,e2} and

P .vertices() = {c,a,b} and

A153: P . 1 = c and

A154: P . 3 = a and

A155: P . 5 = b by A132, A133, A134, A141, A142, A143, A147, A148, CHORD:47;

A156: P .first() = c by A153;

then S_{1}[P]
by A146, A149, A151, A152, A156, A160, A157, A150, CHORD:90;

hence contradiction by A6; :: thesis: verum

end;consider P being Path of G, e1, e2 being object such that

A151: P is open and

A152: len P = 5 and

P .length() = 2 and

e1 Joins c,a,G and

e2 Joins a,b,G and

P .edges() = {e1,e2} and

P .vertices() = {c,a,b} and

A153: P . 1 = c and

A154: P . 3 = a and

A155: P . 5 = b by A132, A133, A134, A141, A142, A143, A147, A148, CHORD:47;

A156: P .first() = c by A153;

A157: now :: thesis: for j, k being odd Element of NAT st 1 <= j & j < k & k <= 3 holds

L . (P . j) > L . (P . k)

L . (P . j) > L . (P . k)

let j, k be odd Element of NAT ; :: thesis: ( 1 <= j & j < k & k <= 3 implies L . (P . j) > L . (P . k) )

assume that

1 <= j and

A158: j < k and

A159: k <= 3 ; :: thesis: L . (P . j) > L . (P . k)

j < 3 by A158, A159, XXREAL_0:2;

then j = 1 by CHORD:7, XXREAL_0:2;

hence L . (P . j) > L . (P . k) by A142, A143, A148, A153, A154, A158, A159, CHORD:7, XXREAL_0:2; :: thesis: verum

end;assume that

1 <= j and

A158: j < k and

A159: k <= 3 ; :: thesis: L . (P . j) > L . (P . k)

j < 3 by A158, A159, XXREAL_0:2;

then j = 1 by CHORD:7, XXREAL_0:2;

hence L . (P . j) > L . (P . k) by A142, A143, A148, A153, A154, A158, A159, CHORD:7, XXREAL_0:2; :: thesis: verum

A160: now :: thesis: for j, k being odd Element of NAT st 3 <= j & j < k & k <= len P holds

L . (P . j) < L . (P . k)

P .last() = b
by A152, A155;L . (P . j) < L . (P . k)

let j, k be odd Element of NAT ; :: thesis: ( 3 <= j & j < k & k <= len P implies L . (P . j) < L . (P . k) )

assume that

A161: 3 <= j and

A162: j < k and

A163: k <= len P ; :: thesis: L . (P . j) < L . (P . k)

j < 5 by A152, A162, A163, XXREAL_0:2;

then ( j = 1 or j = 3 or j = 5 ) by CHORD:8, XXREAL_0:2;

hence L . (P . j) < L . (P . k) by A141, A142, A143, A147, A148, A152, A153, A154, A155, A161, A162, A163, CHORD:8, XXREAL_0:2; :: thesis: verum

end;assume that

A161: 3 <= j and

A162: j < k and

A163: k <= len P ; :: thesis: L . (P . j) < L . (P . k)

j < 5 by A152, A162, A163, XXREAL_0:2;

then ( j = 1 or j = 3 or j = 5 ) by CHORD:8, XXREAL_0:2;

hence L . (P . j) < L . (P . k) by A141, A142, A143, A147, A148, A152, A153, A154, A155, A161, A162, A163, CHORD:8, XXREAL_0:2; :: thesis: verum

then S

hence contradiction by A6; :: thesis: verum

suppose A164:
L . c < L . b
; :: thesis: contradiction

A165:
(2 * 1) + 1 is odd
;

consider P being Path of G, e1, e2 being object such that

A166: P is open and

A167: len P = 5 and

P .length() = 2 and

e1 Joins b,a,G and

e2 Joins a,c,G and

P .edges() = {e1,e2} and

P .vertices() = {b,a,c} and

A168: P . 1 = b and

A169: P . 3 = a and

A170: P . 5 = c by A132, A133, A134, A141, A142, A143, A147, A148, CHORD:47;

A171: P .first() = b by A168;

then S_{1}[P]
by A146, A164, A166, A167, A171, A175, A172, A165, CHORD:90;

hence contradiction by A6; :: thesis: verum

end;consider P being Path of G, e1, e2 being object such that

A166: P is open and

A167: len P = 5 and

P .length() = 2 and

e1 Joins b,a,G and

e2 Joins a,c,G and

P .edges() = {e1,e2} and

P .vertices() = {b,a,c} and

A168: P . 1 = b and

A169: P . 3 = a and

A170: P . 5 = c by A132, A133, A134, A141, A142, A143, A147, A148, CHORD:47;

A171: P .first() = b by A168;

A172: now :: thesis: for j, k being odd Element of NAT st 1 <= j & j < k & k <= 3 holds

L . (P . j) > L . (P . k)

L . (P . j) > L . (P . k)

let j, k be odd Element of NAT ; :: thesis: ( 1 <= j & j < k & k <= 3 implies L . (P . j) > L . (P . k) )

assume that

1 <= j and

A173: j < k and

A174: k <= 3 ; :: thesis: L . (P . j) > L . (P . k)

j < 3 by A173, A174, XXREAL_0:2;

then j = 1 by CHORD:7, XXREAL_0:2;

hence L . (P . j) > L . (P . k) by A141, A143, A147, A168, A169, A173, A174, CHORD:7, XXREAL_0:2; :: thesis: verum

end;assume that

1 <= j and

A173: j < k and

A174: k <= 3 ; :: thesis: L . (P . j) > L . (P . k)

j < 3 by A173, A174, XXREAL_0:2;

then j = 1 by CHORD:7, XXREAL_0:2;

hence L . (P . j) > L . (P . k) by A141, A143, A147, A168, A169, A173, A174, CHORD:7, XXREAL_0:2; :: thesis: verum

A175: now :: thesis: for j, k being odd Element of NAT st 3 <= j & j < k & k <= len P holds

L . (P . j) < L . (P . k)

P .last() = c
by A167, A170;L . (P . j) < L . (P . k)

let j, k be odd Element of NAT ; :: thesis: ( 3 <= j & j < k & k <= len P implies L . (P . j) < L . (P . k) )

assume that

A176: 3 <= j and

A177: j < k and

A178: k <= len P ; :: thesis: L . (P . j) < L . (P . k)

j < 5 by A167, A177, A178, XXREAL_0:2;

then ( j = 1 or j = 3 or j = 5 ) by CHORD:8, XXREAL_0:2;

hence L . (P . j) < L . (P . k) by A141, A142, A143, A147, A148, A167, A168, A169, A170, A176, A177, A178, CHORD:8, XXREAL_0:2; :: thesis: verum

end;assume that

A176: 3 <= j and

A177: j < k and

A178: k <= len P ; :: thesis: L . (P . j) < L . (P . k)

j < 5 by A167, A177, A178, XXREAL_0:2;

then ( j = 1 or j = 3 or j = 5 ) by CHORD:8, XXREAL_0:2;

hence L . (P . j) < L . (P . k) by A141, A142, A143, A147, A148, A167, A168, A169, A170, A176, A177, A178, CHORD:8, XXREAL_0:2; :: thesis: verum

then S

hence contradiction by A6; :: thesis: verum