let G be finite chordal _Graph; :: thesis:
let L be PartFunc of (the_Vertices_of G),NAT ; :: thesis:
assume that
A1: L is with_property_T and
A2: dom L = the_Vertices_of G ; :: thesis:
let V be VertexScheme of G; :: thesis:
assume A3: V " = L ; :: thesis:
A4: V is one-to-one by CHORD:def 12;
A6: L " = V by A3, A4, FUNCT_1:65;
len V = card (the_Vertices_of G) by CHORD:104;
then dom V = Seg (G .order() ) by FINSEQ_1:def 3;
then A7: rng L = Seg (G .order() ) by A3, A4, FUNCT_1:55;
defpred S₁[ Path of G] means ( len $1 >= 5 & not $1 is closed & not $1 is chordal & 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) ) ) );

A8: now

let R be Path of G; :: thesis:
assume A9: S₁[R] ; :: thesis:
defpred S₂[ Nat] means ex P being Path of G st
( S₁[P] & L . (P .last() ) = $1 );
A10: for k being Nat st S₂[k] holds
k <= G .order()

proof

let k be Nat; :: thesis:
assume A11: S₂[k] ; :: thesis:
consider P being Path of G such that
A12: ( S₁[P] & L . (P .last() ) = k ) by A11;
L . (P .last() ) in Seg (G .order() ) by A2, A7, FUNCT_1:def 5;
hence k <= G .order() by A12, FINSEQ_1:3; :: thesis:

end;

A13: ex k being Nat st S₂[k] by A9;
consider k being Nat such that
A14: S₂[k] and
A15: for n being Nat st S₂[n] holds
n <= k from NAT_1:sch 6(A10, A13);
consider P being Path of G such that
A16: ( S₁[P] & L . (P .last() ) = k ) by A14;
consider i being odd Element of NAT such that
A17: ( 1 < i & i < len P ) and
A18: for j, k being odd Element of NAT st i <= j & j < k & k <= len P holds
L . (P . j) < L . (P . k) and
A19: for j, k being odd Element of NAT st 1 <= j & j < k & k <= i holds
L . (P . j) > L . (P . k) by A16;
reconsider c = P .first() as Vertex of G ;
reconsider b = P .last() as Vertex of G ;
3 <= len P by A16, 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 ;
A20: ( (2 * 0 ) + 1 < (2 * 1) + 1 & 3 < len P ) by A16, XXREAL_0:2;
then consider ez being set such that
A21: ez Joins P . 1,P . 3,G by A16, CHORD:92;
A22: c,a are_adjacent by A21, CHORD:def 3;

A23: now

let e be set ; :: thesis:
assume A24: e Joins c,b,G ; :: thesis:
(2 * 0 ) + 1 < len P by A16, XXREAL_0:2;
then ( ex e being set st e Joins P . 1,P . (len P),G iff 1 + 2 = len P ) by A16, CHORD:92;
hence contradiction by A16, A24; :: thesis:

end;

then A25: not b,c are_adjacent by CHORD:def 3;
then consider d being Vertex of G such that
A26: ( d in dom L & L . b < L . d ) and
A27: ( b,d are_adjacent & not a,d are_adjacent ) by A1, A2, A16, A22, Def41;
A28: d <> c by A23, A27, CHORD:def 3;
A29: L . a < L . d by A16, A26, XXREAL_0:2;

A30: now

assume d in P .vertices() ; :: thesis:
then consider dn being odd Element of NAT such that
A31: ( dn <= len P & P . dn = d ) by GLIB_001:88;
A32: dn < len P by A26, A31, XXREAL_0:1;
( dn <> 1 & 1 <= dn ) by A23, A27, A31, CHORD:2, CHORD:def 3;
then (2 * 0 ) + 1 < dn by XXREAL_0:1;
then ( 1 + 2 <= dn & dn <> 3 ) by A16, A26, A31, CHORD:4;
then A33: (2 * 1) + 1 < dn by XXREAL_0:1;

per cases ;

suppose i <= dn ; :: thesis:

hence contradiction by A18, A26, A31, A32; :: thesis:

end;

suppose dn < i ; :: thesis:

hence contradiction by A19, A29, A31, A33; :: thesis:

end;

A34: L . d <> L . c by A2, A3, A4, A25, A27, FUNCT_1:def 8;
defpred S₃[ Nat] means ( not $1 is even & 3 < $1 & $1 <= len P & ex e being set st e Joins P . $1,d,G );
consider el being set such that
A35: el Joins P .last() ,d,G by A27, CHORD:def 3;
A36: ex k being Nat st S₃[k] by A20, A35;
ex j being Nat st
( S₃[j] & ( for n being Nat st S₃[n] holds
j <= n ) ) from NAT_1:sch 5(A36);
then consider j being Nat such that
A37: ( not j is even & 3 < j & j <= len P & ex e being set st e Joins P . j,d,G ) and
A38: for i being Nat st S₃[i] holds
j <= i ;
reconsider j = j as odd Element of NAT by A37, ORDINAL1:def 13;
consider e being set such that
A39: e Joins P . j,d,G by A37;
A40: (2 * 0 ) + 1 <= j by CHORD:2;
reconsider C = P .cut 1,j as Path of G ;
A41: (len C) + 1 = j + 1 by A37, A40, GLIB_001:37;
A42: ( C .first() = P .first() & C .last() = P . j ) by A37, A40, GLIB_001:38;
C .vertices() c= P .vertices() by A37, A40, GLIB_001:95;
then A43: not d in C .vertices() by A30;
A44: e Joins C .last() ,d,G by A37, A39, A40, GLIB_001:38;

A45: now

let n be odd Element of NAT ; :: thesis:
assume A46: n <= j ; :: thesis:
1 <= n by CHORD:2;
then n in dom C by A41, A46, FINSEQ_3:27;
then C . n = P . ((1 + n) - 1) by A37, A40, GLIB_001:48;
hence C . n = P . n ; :: thesis:

end;

(2 * 0 ) + 1 < j by A37, XXREAL_0:2;
then A47: ( not C is closed & not C is chordal ) by A16, A37, CHORD:93;
(2 * 1) + 1 < j by A37;
then A48: ( C . 3 = a & 3 in dom C ) by A41, A45, FINSEQ_3:27;

A49: now

let f be set ; :: thesis:
assume A50: f Joins C . ((len C) - 2),d,G ; :: thesis:
len C > (2 * 1) + 1 by A37, A41;
then A51: len C >= 3 + 2 by CHORD:4;
len C <> 5 by A27, A48, A50, CHORD:def 3;
then len C > 5 by A51, XXREAL_0:1;
then A52: (3 + 2) - 2 < (len C) - 2 by XREAL_1:11;
then 0 < (len C) - (2 * 1) ;
then reconsider cc = (len C) - 2 as odd Element of NAT by INT_1:16;
A53: ( 3 < cc & cc < len C ) by A52, XREAL_1:46;
then A54: cc < len P by A37, A41, XXREAL_0:2;
f Joins P . cc,d,G by A41, A45, A50, A53;
hence contradiction by A38, A41, A53, A54; :: thesis:

end;

then reconsider D = C .addEdge e as Path of G by A43, A44, A47, CHORD:97;
A55: ( not D is closed & not D is chordal ) by A43, A44, A47, A49, CHORD:97;
A56: len D = (len C) + 2 by A39, A42, GLIB_001:65;
then A57: len D >= 3 + 2 by A37, A41, XREAL_1:9;
A58: ( D .first() = c & D .last() = d ) by A39, A42, GLIB_001:64;
A59: D . 3 = a by A39, A42, A48, GLIB_001:66;

A60: now

let n be odd Nat; :: thesis:
assume A61: n <= j ; :: thesis:
1 <= n by CHORD:2;
then n in dom C by A41, A61, FINSEQ_3:27;
hence C . n = D . n by A44, GLIB_001:66; :: thesis:

end;

A62: 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) ) )

proof

per cases ;

suppose A63: j <= i ; :: thesis:

take j ; :: thesis:

A64: now

let e, f be odd Element of NAT ; :: thesis:
assume A65: ( j <= e & e < f & f <= len D ) ; :: thesis:
e < j + (2 * 1) by A41, A56, A65, XXREAL_0:2;
then e <= (j + 2) - 2 by CHORD:3;
then A66: e = j by A65, XXREAL_0:1;
then D . e = C . j by A60;
then A67: D . e = P . j by A45;
(len C) + 2 <= f by A41, A65, A66, CHORD:4;
then A68: D . f = d by A56, A58, A65, XXREAL_0:1;
( 1 < (2 * 1) + 1 & 3 < j ) by A37;
then L . (P . 3) > L . (P . j) by A19, A63;
hence L . (D . e) < L . (D . f) by A29, A67, A68, XXREAL_0:2; :: thesis:

end;

now

let e, f be odd Element of NAT ; :: thesis:
assume A69: ( 1 <= e & e < f & f <= j ) ; :: thesis:
( e <= j & D . e = C . e ) by A60, A69, XXREAL_0:2;
then A70: D . e = P . e by A45;
D . f = C . f by A60, A69;
then A71: D . f = P . f by A45, A69;
f <= i by A63, A69, XXREAL_0:2;
hence L . (D . e) > L . (D . f) by A19, A69, A70, A71; :: thesis:

end;

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 . 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 A37, A41, A56, A64, XREAL_1:31, XXREAL_0:2; :: thesis:

end;

suppose A72: i < j ; :: thesis:

take i ; :: thesis:
A73: len D > j by A41, A56, XREAL_1:31;

A74: now

let e, f be odd Element of NAT ; :: thesis:
assume A75: ( i <= e & e < f & f <= len D ) ; :: thesis:
e < j + (2 * 1) by A41, A56, A75, XXREAL_0:2;
then A76: e <= (j + 2) - 2 by CHORD:3;
then A77: D . e = C . e by A60;
then A78: D . e = P . e by A45, A76;
A79: e <= len P by A37, A76, XXREAL_0:2;

per cases by A75, XXREAL_0:1;

suppose A80: f = len D ; :: thesis:

now

per cases by A79, XXREAL_0:1;

suppose e = len P ; :: thesis:

hence L . (D . e) <= L . b by A45, A76, A77; :: thesis:

end;

suppose e < len P ; :: thesis:

hence L . (D . e) <= L . b by A18, A75, A78; :: thesis:

end;

hence L . (D . e) < L . (D . f) by A26, A58, A80, XXREAL_0:2; :: thesis:

end;

suppose f < len D ; :: thesis:

then A81: f <= (j + 2) - 2 by A41, A56, CHORD:3;
then D . f = C . f by A60;
then A82: D . f = P . f by A45, A81;
( i <= e & e < f & f <= len P ) by A37, A75, A81, XXREAL_0:2;
hence L . (D . e) < L . (D . f) by A18, A78, A82; :: thesis:

end;

now

let e, f be odd Element of NAT ; :: thesis:
assume A83: ( 1 <= e & e < f & f <= i ) ; :: thesis:
e <= i by A83, XXREAL_0:2;
then ( e <= j & D . e = C . e ) by A60, A72, XXREAL_0:2;
then A84: D . e = P . e by A45;
( f <= j & D . f = C . f ) by A60, A72, A83, XXREAL_0:2;
then D . f = P . f by A45;
hence L . (D . e) > L . (D . f) by A19, A83, A84; :: thesis:

end;

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 A17, A72, A73, A74, XXREAL_0:2; :: thesis:

end;

then L . c <= L . d by A15, A16, A26, A29, A55, A57, A58, A59;
then A85: L . c < L . d by A34, XXREAL_0:1;
reconsider R = D .reverse() as Path of G ;
A86: ( R .first() = d & R .last() = c ) by A58, GLIB_001:23;
then A87: ( not R is closed & not R is chordal ) by A28, A55, CHORD:91, GLIB_001:def 24;
A88: len R >= 3 + 2 by A57, GLIB_001:22;
then 3 <= len R by XXREAL_0:2;
then 3 in dom R by FINSEQ_3:27;
then R . 3 = D . (((len D) - 3) + 1) by GLIB_001:26;
then A89: R . 3 = C . j by A41, A56, A60;

now

per cases ;

suppose A90: i < j ; :: thesis:

now

per cases by A37, XXREAL_0:1;

suppose j = len P ; :: thesis:

hence L . (P . j) <= L . b ; :: thesis:

end;

suppose j < len P ; :: thesis:

hence L . (P . j) <= L . b by A18, A90; :: thesis:

end;

hence L . (P . j) < L . c by A16, XXREAL_0:2; :: thesis:

end;

suppose i >= j ; :: thesis:

then ( 1 < (2 * 1) + 1 & 3 < j & j <= i ) by A37;
then L . (P . j) < L . (P . 3) by A19;
then L . (P . j) < L . b by A16, XXREAL_0:2;
hence L . (P . j) < L . c by A16, XXREAL_0:2; :: thesis:

end;

then A91: L . (R .last() ) > L . (R . 3) by A45, A86, A89;
A92: 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:
assume A93: n <= len R ; :: thesis:
1 <= n by CHORD:2;
then A94: n in dom R by A93, FINSEQ_3:27;
hence R . n = D . (((len D) - n) + 1) by GLIB_001:26; :: thesis:
((len D) - n) + 1 in dom D by A94, GLIB_001:26;
hence ((len D) - n) + 1 is Element of NAT ; :: thesis:

end;

ex i being odd Element of NAT st
( 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

consider i being odd Element of NAT such that
A95: ( 1 < i & i < len D ) and
A96: for j, k being odd Element of NAT st i <= j & j < k & k <= len D holds
L . (D . j) < L . (D . k) and
A97: for j, k being odd Element of NAT st 1 <= j & j < k & k <= i holds
L . (D . j) > L . (D . k) by A62;
set ir = ((len D) - i) + 1;
(len D) - 1 > (len D) - i by A95, XREAL_1:17;
then A98: ((len D) - 1) + 1 > ((len D) - i) + 1 by XREAL_1:10;
A99a: (len D) - (len D) < (len D) - i by A95, XREAL_1:17;
then A99: 0 + 1 < ((len D) - i) + 1 by XREAL_1:10;
then A100: ( 1 < ((len D) - i) + 1 & ((len D) - i) + 1 < len R ) by A98, GLIB_001:22;
reconsider ir = ((len D) - i) + 1 as odd Element of NAT by A99a, INT_1:16;
take ir ; :: thesis:

A101: now

let j, k be odd Element of NAT ; :: thesis:
assume A102: ( ir <= j & j < k & k <= len R ) ; :: thesis:
set jr = ((len D) - j) + 1;
set kr = ((len D) - k) + 1;
A103: ( 1 < j & j <= len R ) by A99, A102, XXREAL_0:2;
then A104: R . j = D . (((len D) - j) + 1) by A92;
reconsider jr = ((len D) - j) + 1 as odd Element of NAT by A92, A103;
A105: R . k = D . (((len D) - k) + 1) by A92, A102;
reconsider kr = ((len D) - k) + 1 as odd Element of NAT by A92, A102;
i + j >= (((len D) - i) + 1) + i by A102, XREAL_1:9;
then (i + j) - j >= ((len D) + 1) - j by XREAL_1:11;
then ( 1 <= kr & kr < jr & jr <= i ) by A102, Lm1, CHORD:2;
hence L . (R . j) < L . (R . k) by A97, A104, A105; :: thesis:

end;

now

let ja, k be odd Element of NAT ; :: thesis:
assume A106: ( 1 <= ja & ja < k & k <= ir ) ; :: thesis:
set jr = ((len D) - ja) + 1;
set kr = ((len D) - k) + 1;
A107: ( 1 < k & k <= len R ) by A100, A106, XXREAL_0:2;
i + k <= (((len D) - i) + 1) + i by A106, XREAL_1:9;
then (i + k) - k <= ((len D) + 1) - k by XREAL_1:11;
then A108: ( i <= ((len D) - k) + 1 & ((len D) - k) + 1 < ((len D) - ja) + 1 ) by A106, Lm1;
reconsider kr = ((len D) - k) + 1 as odd Element of NAT by A92, A107;
A109: ja <= len R by A106, A107, XXREAL_0:2;
then A110: R . ja = D . (((len D) - ja) + 1) by A92;
reconsider jr = ((len D) - ja) + 1 as odd Element of NAT by A92, A109;
(len D) - ja <= (len D) - 1 by A106, XREAL_1:12;
then jr <= ((len D) - 1) + 1 by XREAL_1:9;
then L . (D . kr) < L . (D . jr) by A96, A108;
hence L . (R . ja) > L . (R . k) by A92, A107, A110; :: thesis:

end;

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 A98, A99, A101, GLIB_001:22; :: thesis:

end;

hence contradiction by A15, A16, A85, A86, A87, A88, A91; :: thesis:

end;

now

let a, b, c be Vertex of G; :: thesis:
assume A112: ( b <> c & a,b are_adjacent & a,c are_adjacent ) ; :: thesis:
let va, vb, vc be Nat; :: thesis:
assume that
A113: ( va in dom V & vb in dom V & vc in dom V ) and
A114: ( V . va = a & V . vb = b & V . vc = c & va < vb & va < vc ) ; :: thesis:
assume A115: not b,c are_adjacent ; :: thesis:
A116: ( a = V . (L . a) & b = V . (L . b) & c = V . (L . c) ) by A2, A3, A4, A6, FUNCT_1:56;
A117: ( L . a = va & L . b = vb & L . c = vc ) by A4, A113, A114, A3, FUNCT_1:56;

per cases by A112, A116, XXREAL_0:1;

suppose A118: L . b < L . c ; :: thesis:

consider P being Path of G, e1, e2 being set such that
A119: ( not P is closed & len P = 5 & P .length() = 2 ) and
( e1 Joins c,a,G & e2 Joins a,b,G & P .edges() = {e1,e2} ) and
P .vertices() = {c,a,b} and
A120: ( P . 1 = c & P . 3 = a & P . 5 = b ) by A112, A114, A117, CHORD:47;
A121: ( P .first() = c & P .last() = b ) by A119, A120;

A122: now

let j, k be odd Element of NAT ; :: thesis:
assume A123: ( 3 <= j & j < k & k <= len P ) ; :: thesis:
j < 5 by A119, A123, 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 A114, A117, A119, A120, A123, CHORD:8, XXREAL_0:2; :: thesis:

end;

A124: now

let j, k be odd Element of NAT ; :: thesis:
assume A125: ( 1 <= j & j < k & k <= 3 ) ; :: thesis:
j < 3 by A125, XXREAL_0:2;
then j = 1 by CHORD:7, XXREAL_0:2;
hence L . (P . j) > L . (P . k) by A114, A117, A120, A125, CHORD:7, XXREAL_0:2; :: thesis:

end;

not (2 * 1) + 1 is even ;
then S₁[P] by A115, A118, A119, A121, A122, A124, CHORD:90;
hence contradiction by A8; :: thesis:

end;

suppose A126: L . c < L . b ; :: thesis:

consider P being Path of G, e1, e2 being set such that
A127: ( not P is closed & len P = 5 & P .length() = 2 ) and
( e1 Joins b,a,G & e2 Joins a,c,G & P .edges() = {e1,e2} ) and
P .vertices() = {b,a,c} and
A128: ( P . 1 = b & P . 3 = a & P . 5 = c ) by A112, A114, A117, CHORD:47;
A129: ( P .first() = b & P .last() = c ) by A127, A128;

A130: now

let j, k be odd Element of NAT ; :: thesis:
assume A131: ( 3 <= j & j < k & k <= len P ) ; :: thesis:
j < 5 by A127, A131, 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 A114, A117, A127, A128, A131, CHORD:8, XXREAL_0:2; :: thesis:

end;

A132: now

let j, k be odd Element of NAT ; :: thesis:
assume A133: ( 1 <= j & j < k & k <= 3 ) ; :: thesis:
j < 3 by A133, XXREAL_0:2;
then j = 1 by CHORD:7, XXREAL_0:2;
hence L . (P . j) > L . (P . k) by A114, A117, A128, A133, CHORD:7, XXREAL_0:2; :: thesis:

end;

not (2 * 1) + 1 is even ;
then S₁[P] by A115, A126, A127, A129, A130, A132, CHORD:90;
hence contradiction by A8; :: thesis:

end;

hence V is perfect by CHORD:109; :: thesis: