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_L3 and
A2: dom L = the_Vertices_of G ; :: thesis:
let V be VertexScheme of G; :: thesis:
assume A3: V " = L ; :: thesis:
assume not V is perfect ; :: thesis:
then consider k being non empty Nat such that
A4: k <= len V and
A5: ex H being inducedSubgraph of G,(V .followSet k) ex v being Vertex of H st
( v = V . k & not v is simplicial ) by CHORD:def 13;
consider HH being inducedSubgraph of G,(V .followSet k), hv being Vertex of HH such that
A6: hv = V . k and
A7: not hv is simplicial by A5;
A8: 0 + 1 <= k by NAT_1:13;
A9: V is one-to-one by CHORD:def 12;
A11: rng V = the_Vertices_of G by CHORD:def 12;
consider ha, hb being Vertex of HH such that
A12: ( ha <> hb & hv <> ha & hv <> hb ) and
A13: hv,ha are_adjacent and
A14: hv,hb are_adjacent and
A15: not ha,hb are_adjacent by A7, CHORD:69;
A16: V .followSet k is non empty Subset of (the_Vertices_of G) by A4, CHORD:107;
then A17: the_Vertices_of HH = V .followSet k by GLIB_000:def 39;
( hv in the_Vertices_of HH & ha in the_Vertices_of HH & hb in the_Vertices_of HH ) ;
then reconsider v = hv, aa = ha, bb = hb as Vertex of G ;
A18: for x, y being Vertex of G
for i, j being Nat st i in dom V & j in dom V & V /. i = x & V /. j = y holds
( i < j iff L . x < L . y )

proof

let x, y be Vertex of G; :: thesis:
let i, j be Nat; :: thesis:
assume that
A19: ( i in dom V & j in dom V ) and
A20: ( V /. i = x & V /. j = y ) ; :: thesis:
A21: ( V . i = x & V . j = y ) by A19, A20, PARTFUN1:def 8;
then A22: L . y = j by A3, A9, A19, FUNCT_1:56;
hence ( i < j implies L . x < L . y ) by A3, A9, A19, A21, FUNCT_1:56; :: thesis:
thus ( L . x < L . y implies i < j ) by A3, A9, A19, A21, A22, FUNCT_1:56; :: thesis:

end;

now

A23: L . aa <> L . bb by A2, A9, A3, A12, FUNCT_1:def 8;

per cases by A23, XXREAL_0:1;

suppose A24: L . aa < L . bb ; :: thesis:

take aa = aa; :: thesis:
take bb = bb; :: thesis:
thus aa in V .followSet k by A17; :: thesis:
thus L . aa < L . bb by A24; :: thesis:
thus v,aa are_adjacent by A13, A16, CHORD:45; :: thesis:
thus v,bb are_adjacent by A14, A16, CHORD:45; :: thesis:
thus not aa,bb are_adjacent by A15, A16, CHORD:45; :: thesis:

end;

suppose A25: L . aa > L . bb ; :: thesis:

take bb = bb; :: thesis:
take aa = aa; :: thesis:
thus bb in V .followSet k by A17; :: thesis:
thus L . aa > L . bb by A25; :: thesis:
thus v,bb are_adjacent by A14, A16, CHORD:45; :: thesis:
thus v,aa are_adjacent by A13, A16, CHORD:45; :: thesis:
thus not bb,aa are_adjacent by A15, A16, CHORD:45; :: thesis:

end;

then consider a, bb being Vertex of G such that
A26: a in V .followSet k and
A27: L . a < L . bb and
A28: v,a are_adjacent and
A29: v,bb are_adjacent and
A30: not a,bb are_adjacent ;
defpred S₁[ Nat] means ( $1 in dom V & L . a < L . (V /. $1) & a <> V /. $1 & v,V /. $1 are_adjacent & not a,V /. $1 are_adjacent );
A31: for k being Nat st S₁[k] holds
k <= len V by FINSEQ_3:27;
A32: ex k being Nat st S₁[k]

proof

consider mbb being set such that
A33: ( mbb in dom V & bb = V . mbb ) by A11, FUNCT_1:def 5;
reconsider mbb = mbb as Element of NAT by A33;
take mbb ; :: thesis:
thus mbb in dom V by A33; :: thesis:
thus L . a < L . (V /. mbb) by A27, A33, PARTFUN1:def 8; :: thesis:
thus a <> V /. mbb by A27, A33, PARTFUN1:def 8; :: thesis:
thus v,V /. mbb are_adjacent by A29, A33, PARTFUN1:def 8; :: thesis:
thus not a,V /. mbb are_adjacent by A30, A33, PARTFUN1:def 8; :: thesis:

end;

consider mb being Nat such that
A34: S₁[mb] and
for n being Nat st S₁[n] holds
n <= mb from NAT_1:sch 6(A31, A32);
reconsider v = v, a = a, b = V /. mb as Vertex of G ;
A35: v <> b by A28, A34;
A36: k in dom V by A4, A8, FINSEQ_3:27;
then A37: v = V /. k by A6, PARTFUN1:def 8;
consider ma being set such that
A38: ( ma in dom V & a = V . ma ) by A11, FUNCT_1:def 5;
reconsider ma = ma as Element of NAT by A38;
A39: a = V /. ma by A38, PARTFUN1:def 8;

A40: now

assume ma <= k ; :: thesis:
then A41: ma < k by A6, A29, A30, A38, XXREAL_0:1;
a in the_Vertices_of G ;
then ( a in rng V & V is one-to-one ) by CHORD:def 12;
then a .. V >= k by A26, A36, CHORD:16;
then a .. V > ma by A41, XXREAL_0:2;
hence contradiction by A38, FINSEQ_4:34; :: thesis:

end;

defpred S₂[ Nat] means ex P being Walk of G ex v1, v2, v3, v4 being Vertex of G st
( P is Path-like & not P is closed & not P is chordal & P .length() = $1 - 1 & v1 = P . ((len P) - 2) & v2 = P . 3 & v3 = P .last() & v4 = P .first() & L . v4 > L . v3 & L . v3 > L . v2 & L . v2 > L . v1 & ( for x being set st x in P .vertices() holds
L . x <= L . v4 ) & ( for x being Vertex of G st x <> v4 & x,v2 are_adjacent & not x,v1 are_adjacent holds
L . x < L . v4 ) );
A42: L . v < L . a by A18, A36, A37, A38, A39, A40;
A43: S₂[4]

proof

consider c being Vertex of G such that
A44: ( c in dom L & L . b < L . c ) and
A45: ( c,a are_adjacent & not c,v are_adjacent ) and
A46: for x being Vertex of G st x <> c & x,a are_adjacent & not x,v are_adjacent holds
L . x < L . c by A1, A2, A34, A42, Def34;
consider P being Path of G, e1, e2 being set such that
A47: ( not P is closed & len P = 5 & P .length() = 2 ) and
A48: ( e1 Joins b,v,G & e2 Joins v,a,G & P .edges() = {e1,e2} & P .vertices() = {b,v,a} ) and
A49: ( P . 1 = b & P . 3 = v & P . 5 = a ) by A28, A34, A35, CHORD:47;
( P .first() = b & P .last() = a ) by A47, A49;
then A50: not P is chordal by A34, A47, CHORD:90;
consider e being set such that
A51: e Joins P .last() ,c,G by A45, A47, A49, CHORD:def 3;
set Qr = P .addEdge e;
set Q = (P .addEdge e) .reverse() ;
A52: (P .addEdge e) .length() = 2 + 1 by A47, A51, Lm4;
A53: len (P .addEdge e) = 5 + 2 by A47, A51, GLIB_001:65;
( 1 in dom P & 3 in dom P & 5 in dom P ) by A47, FINSEQ_3:27;
then A54: ( (P .addEdge e) . 1 = b & (P .addEdge e) . 3 = v & (P .addEdge e) . 5 = a ) by A49, A51, GLIB_001:66;
A55: (P .addEdge e) .last() = c by A51, GLIB_001:64;

A56: now

let x be set ; :: thesis:
assume A57: x in P .vertices() ; :: thesis:

per cases by A48, A57, ENUMSET1:def 1;

suppose x = b ; :: thesis:

hence L . x <= L . b ; :: thesis:

end;

suppose x = v ; :: thesis:

hence L . x <= L . b by A34, A42, XXREAL_0:2; :: thesis:

end;

suppose x = a ; :: thesis:

hence L . x <= L . b by A34; :: thesis:

end;

then A58: not c in P .vertices() by A44;
for e being set holds not e Joins P . ((len P) - 2),c,G by A45, A47, A49, CHORD:def 3;
then ( P .addEdge e is Path-like & not P .addEdge e is closed & not P .addEdge e is chordal ) by A47, A50, A51, A58, CHORD:97;
then A59: ( (P .addEdge e) .reverse() is Path-like & not (P .addEdge e) .reverse() is closed & not (P .addEdge e) .reverse() is chordal ) by CHORD:91, GLIB_001:121;
A60: ( 1 in dom (P .addEdge e) & 3 in dom (P .addEdge e) & 5 in dom (P .addEdge e) & 7 in dom (P .addEdge e) ) by A53, FINSEQ_3:27;
A61: ((P .addEdge e) .reverse() ) .length() = (3 + 1) - 1 by A52, Lm5;
A62: ( dom ((P .addEdge e) .reverse() ) = dom (P .addEdge e) & len ((P .addEdge e) .reverse() ) = len (P .addEdge e) ) by GLIB_001:22;
( v = ((P .addEdge e) .reverse() ) . ((7 - 3) + 1) & a = ((P .addEdge e) .reverse() ) . ((7 - 5) + 1) & b = ((P .addEdge e) .reverse() ) . (((len (P .addEdge e)) - 1) + 1) & c = ((P .addEdge e) .reverse() ) . ((7 - 7) + 1) ) by A53, A54, A55, A60, GLIB_001:25;
then A63: ( v = ((P .addEdge e) .reverse() ) . ((len ((P .addEdge e) .reverse() )) - 2) & a = ((P .addEdge e) .reverse() ) . 3 & b = ((P .addEdge e) .reverse() ) .last() & c = ((P .addEdge e) .reverse() ) .first() ) by A53, A62;
A64: ( L . c > L . b & L . b > L . a & L . a > L . v ) by A18, A34, A36, A37, A38, A39, A40, A44;

now

let x be set ; :: thesis:
assume A65: x in ((P .addEdge e) .reverse() ) .vertices() ; :: thesis:
x in (P .addEdge e) .vertices() by A65, GLIB_001:93;
then A66: x in (P .vertices() ) \/ {c} by A51, GLIB_001:96;

per cases by A66, XBOOLE_0:def 3;

suppose x in P .vertices() ; :: thesis:

then L . x <= L . b by A56;
hence L . x <= L . c by A44, XXREAL_0:2; :: thesis:

end;

suppose x in {c} ; :: thesis:

hence L . x <= L . c by TARSKI:def 1; :: thesis:

end;

hence S₂[4] by A46, A59, A61, A63, A64; :: thesis:

end;

A67: for k being Nat st 4 <= k & S₂[k] holds
S₂[k + 1]

proof

let kk be Nat; :: thesis:
assume that
A68: 4 <= kk and
A69: S₂[kk] ; :: thesis:
reconsider k = kk as non empty Nat by A68;
consider P being Walk of G, v1, v2, v3, v4 being Vertex of G such that
A70: ( P is Path-like & not P is closed & not P is chordal & P .length() = k - 1 ) and
A71: ( v1 = P . ((len P) - 2) & v2 = P . 3 & v3 = P .last() & v4 = P .first() ) and
A72: ( L . v4 > L . v3 & L . v3 > L . v2 & L . v2 > L . v1 ) and
A73: for x being set st x in P .vertices() holds
L . x <= L . v4 and
A74: for x being Vertex of G st x <> v4 & x,v2 are_adjacent & not x,v1 are_adjacent holds
L . x < L . v4 by A69;
A75: len P = (2 * (k - 1)) + 1 by A70, GLIB_001:113;
2 * k >= 2 * 4 by A68, XREAL_1:66;
then A76: (2 * k) - 1 >= 8 - 1 by XREAL_1:11;
then ( (2 * 0 ) + 1 < (2 * 1) + 1 & 3 < len P ) by A75, XXREAL_0:2;
then consider ez being set such that
A77: ez Joins P . 1,P . 3,G by A70, CHORD:92;

now

let e be set ; :: thesis:
assume A78: e Joins v4,v3,G ; :: thesis:
(2 * 0 ) + 1 < len P by A75, A76, XXREAL_0:2;
then 1 + 2 = len P by A70, A71, A78, CHORD:92;
hence contradiction by A68, A75; :: thesis:

end;

then ( v4,v2 are_adjacent & not v4,v3 are_adjacent ) by A71, A77, CHORD:def 3;
then consider v5 being Vertex of G such that
A79: ( v5 in dom L & L . v4 < L . v5 ) and
A80: ( v5,v3 are_adjacent & not v5,v2 are_adjacent ) and
A81: for x being Vertex of G st x <> v5 & x,v3 are_adjacent & not x,v2 are_adjacent holds
L . x < L . v5 by A1, A2, A72, Def34;

A82: now

assume A83: v5,v1 are_adjacent ; :: thesis:
L . v2 < L . v4 by A72, XXREAL_0:2;
then ( L . v1 < L . v2 & L . v2 < L . v5 ) by A72, A79, XXREAL_0:2;
then consider v6 being Vertex of G such that
A84: ( v6 in dom L & L . v5 < L . v6 ) and
A85: ( v6,v2 are_adjacent & not v6,v1 are_adjacent ) and
for x being Vertex of G st x <> v6 & x,v2 are_adjacent & not x,v1 are_adjacent holds
L . x < L . v6 by A1, A2, A80, A83, Def34;
thus contradiction by A74, A79, A84, A85, XXREAL_0:2; :: thesis:

end;

consider e being set such that
A86: e Joins P .last() ,v5,G by A71, A80, CHORD:def 3;
set Qr = P .addEdge e;
set Q = (P .addEdge e) .reverse() ;
A87: (P .addEdge e) .length() = (k - 1) + 1 by A70, A86, Lm4;
A88: len (P .addEdge e) = (len P) + 2 by A86, GLIB_001:65;
1 <= len P by A75, A76, XXREAL_0:2;
then ( P . ((len (P .addEdge e)) - 2) = v3 & len P in dom P ) by A71, A88, FINSEQ_3:27;
then A89: ( v3 = (P .addEdge e) . ((len (P .addEdge e)) - 2) & (len (P .addEdge e)) - 2 in dom (P .addEdge e) ) by A86, A88, Lm6;
( 1 <= 3 & 3 <= len P ) by A75, A76, XXREAL_0:2;
then 3 in dom P by FINSEQ_3:27;
then A90: ( v2 = (P .addEdge e) . 3 & 3 in dom (P .addEdge e) ) by A71, A86, Lm6;
A91: ( v4 = (P .addEdge e) .first() & v5 = (P .addEdge e) .last() ) by A71, A86, GLIB_001:64;
A92: not v5 in P .vertices() by A73, A79;
for e being set holds not e Joins P . ((len P) - 2),v5,G by A71, A82, CHORD:def 3;
then ( P .addEdge e is Path-like & not P .addEdge e is closed & not P .addEdge e is chordal ) by A70, A86, A92, CHORD:97;
then A93: ( (P .addEdge e) .reverse() is Path-like & not (P .addEdge e) .reverse() is closed & not (P .addEdge e) .reverse() is chordal ) by CHORD:91, GLIB_001:121;
A94: ((P .addEdge e) .reverse() ) .length() = (k + 1) - 1 by A87, Lm5;
A95: len ((P .addEdge e) .reverse() ) = len (P .addEdge e) by GLIB_001:22;
then ( v2 = ((P .addEdge e) .reverse() ) . (((len ((P .addEdge e) .reverse() )) - 3) + 1) & v3 = ((P .addEdge e) .reverse() ) . (((len ((P .addEdge e) .reverse() )) - ((len (P .addEdge e)) - 2)) + 1) ) by A89, A90, GLIB_001:25;
then A96: ( v2 = ((P .addEdge e) .reverse() ) . ((len ((P .addEdge e) .reverse() )) - 2) & v3 = ((P .addEdge e) .reverse() ) . 3 & v4 = ((P .addEdge e) .reverse() ) .last() & v5 = ((P .addEdge e) .reverse() ) .first() ) by A91, A95, GLIB_001:23;

now

let x be set ; :: thesis:
assume A97: x in ((P .addEdge e) .reverse() ) .vertices() ; :: thesis:
x in (P .addEdge e) .vertices() by A97, GLIB_001:93;
then A98: x in (P .vertices() ) \/ {v5} by A86, GLIB_001:96;

per cases by A98, XBOOLE_0:def 3;

suppose x in P .vertices() ; :: thesis:

then L . x <= L . v4 by A73;
hence L . x <= L . v5 by A79, XXREAL_0:2; :: thesis:

end;

suppose x in {v5} ; :: thesis:

hence L . x <= L . v5 by TARSKI:def 1; :: thesis:

end;

hence S₂[kk + 1] by A72, A79, A81, A93, A94, A96; :: thesis:

end;

A99: for i being Nat st 4 <= i holds
S₂[i] from NAT_1:sch 8(A43, A67);
( 4 <= 11 & 11 <= 11 + (G .order() ) ) by NAT_1:11;
then S₂[(G .order() ) + 11] by A99, XXREAL_0:2;
then consider P being Walk of G, v1, v2, v3, v4 being Vertex of G such that
A100: ( P is Path-like & not P is closed & not P is chordal ) and
A101: P .length() = ((G .order() ) + 11) - 1 and
( v1 = P . ((len P) - 2) & v2 = P . 3 & v3 = P .last() & v4 = P .first() ) and
( L . v4 > L . v3 & L . v3 > L . v2 & L . v2 > L . v1 ) and
for x being Vertex of G st x <> v4 & x,v2 are_adjacent & not x,v1 are_adjacent holds
L . x < L . v4 ;
len P = (2 * ((G .order() ) + 10)) + 1 by A101, GLIB_001:113;
then ((2 * (G .order() )) + 21) + 1 = 2 * (len (P .vertexSeq() )) by GLIB_001:def 14;
then (G .order() ) + 11 <= (G .order() ) + 1 by A100, GLIB_001:155;
hence contradiction by XREAL_1:10; :: thesis: