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:
A4: V is one-to-one by CHORD:def 12;
A5: 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 )

let x, y be Vertex of G; :: thesis:
let i, j be Nat; :: thesis:
assume that
A6: i in dom V and
A7: j in dom V and
A8: V /. i = x and
A9: V /. j = y ; :: thesis:
V . j = y by A7, A9, PARTFUN1:def 6;
then A10: L . y = j by A3, A4, A7, FUNCT_1:34;
A11: V . i = x by A6, A8, PARTFUN1:def 6;
hence ( i < j implies L . x < L . y ) by A3, A4, A6, A10, FUNCT_1:34; :: thesis:
thus ( L . x < L . y implies i < j ) by A3, A4, A6, A11, A10, FUNCT_1: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 & P is open & P is chordless & 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 ) );
A12: for k being Nat st 4 <= k & S₁[k] holds
S₁[k + 1]

proof

A13: (2 * 0) + 1 < (2 * 1) + 1 ;
let kk be Nat; :: thesis:
assume that
A14: 4 <= kk and
A15: S₁[kk] ; :: thesis:
reconsider k = kk as non zero Nat by A14;
consider P being Walk of G, v1, v2, v3, v4 being Vertex of G such that
A16: P is Path-like and
A17: P is open and
A18: P is chordless and
A19: P .length() = k - 1 and
A20: v1 = P . ((len P) - 2) and
A21: v2 = P . 3 and
A22: v3 = P .last() and
A23: v4 = P .first() and
A24: L . v4 > L . v3 and
A25: L . v3 > L . v2 and
A26: L . v2 > L . v1 and
A27: for x being set st x in P .vertices() holds
L . x <= L . v4 and
A28: for x being Vertex of G st x <> v4 & x,v2 are_adjacent & not x,v1 are_adjacent holds
L . x < L . v4 by A15;
A29: len P = (2 * (k - 1)) + 1 by A19, GLIB_001:112;
2 * k >= 2 * 4 by A14, XREAL_1:64;
then A30: (2 * k) - 1 >= 8 - 1 by XREAL_1:9;
then 1 <= len P by A29, XXREAL_0:2;
then A31: len P in dom P by FINSEQ_3:25;

now :: thesis:

A32: (2 * 0) + 1 < len P by A29, A30, XXREAL_0:2;
let e be object ; :: thesis:
assume e Joins v4,v3,G ; :: thesis:
then 1 + 2 = len P by A16, A17, A18, A22, A23, A32, CHORD:92;
hence contradiction by A14, A29; :: thesis:

end;

then A33: not v4,v3 are_adjacent by CHORD:def 3;
3 < len P by A29, A30, XXREAL_0:2;
then ex ez being object st ez Joins P . 1,P . 3,G by A16, A17, A18, A13, CHORD:92;
then v4,v2 are_adjacent by A21, A23, CHORD:def 3;
then consider v5 being Vertex of G such that
v5 in dom L and
A34: L . v4 < L . v5 and
A35: v5,v3 are_adjacent and
A36: not v5,v2 are_adjacent and
A37: 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, A24, A25, A33;
consider e being object such that
A38: e Joins P .last() ,v5,G by A22, A35, CHORD:def 3;

now :: thesis:

L . v2 < L . v4 by A24, A25, XXREAL_0:2;
then A39: L . v2 < L . v5 by A34, XXREAL_0:2;
assume v5,v1 are_adjacent ; :: thesis:
then consider v6 being Vertex of G such that
v6 in dom L and
A40: L . v5 < L . v6 and
A41: v6,v2 are_adjacent and
A42: 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, A26, A36, A39;
thus contradiction by A28, A34, A40, A41, A42, XXREAL_0:2; :: thesis:

end;

A57: now :: thesis:

let x be set ; :: thesis:
assume x in ((P .addEdge e) .reverse()) .vertices() ; :: thesis:
then x in (P .addEdge e) .vertices() by GLIB_001:92;
then A58: x in (P .vertices()) \/ {v5} by A38, GLIB_001:95;

per cases by A58, XBOOLE_0:def 3;

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

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

end;

suppose x in {v5} ; :: thesis:

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

end;

P .addEdge e is Path-like by A16, A17, A18, A38, A45, A43, CHORD:97;
hence S₁[kk + 1] by A24, A25, A34, A37, A46, A55, A56, A44, A49, A53, A50, A54, A57; :: thesis:

end;

A59: 11 <= 11 + (G .order()) by NAT_1:11;
assume not V is perfect ; :: thesis:
then consider k being non zero Nat such that
A60: k <= len V and
A61: 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
A62: hv = V . k and
A63: not hv is simplicial by A61;
consider ha, hb being Vertex of HH such that
A64: ha <> hb and
hv <> ha and
hv <> hb and
A65: hv,ha are_adjacent and
A66: hv,hb are_adjacent and
A67: not ha,hb are_adjacent by A63, CHORD:69;
A68: hv in the_Vertices_of HH ;
A69: hb in the_Vertices_of HH ;
ha in the_Vertices_of HH ;
then reconsider v = hv, aa = ha, bb = hb as Vertex of G by A68, A69;
A70: V .followSet k is non empty Subset of (the_Vertices_of G) by A60, CHORD:107;
then A71: the_Vertices_of HH = V .followSet k by GLIB_000:def 37;

now :: thesis:

A72: L . aa <> L . bb by A2, A3, A4, A64, FUNCT_1:def 4;

per cases by A72, XXREAL_0:1;

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

take aa = aa; :: thesis:
take bb = bb; :: thesis:
thus aa in V .followSet k by A71; :: thesis:
thus L . aa < L . bb by A73; :: thesis:
thus v,aa are_adjacent by A65, A70, CHORD:45; :: thesis:
thus v,bb are_adjacent by A66, A70, CHORD:45; :: thesis:
thus not aa,bb are_adjacent by A67, A70, CHORD:45; :: thesis:

end;

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

take bb = bb; :: thesis:
take aa = aa; :: thesis:
thus bb in V .followSet k by A71; :: thesis:
thus L . aa > L . bb by A74; :: thesis:
thus v,bb are_adjacent by A66, A70, CHORD:45; :: thesis:
thus v,aa are_adjacent by A65, A70, CHORD:45; :: thesis:
thus not bb,aa are_adjacent by A67, A70, CHORD:45; :: thesis:

end;

then consider a, bb being Vertex of G such that
A75: a in V .followSet k and
A76: L . a < L . bb and
A77: v,a are_adjacent and
A78: v,bb are_adjacent and
A79: 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 );
A80: rng V = the_Vertices_of G by CHORD:def 12;
A81: ex k being Nat st S₂[k]

proof

consider mbb being object such that
A82: mbb in dom V and
A83: bb = V . mbb by A80, FUNCT_1:def 3;
reconsider mbb = mbb as Element of NAT by A82;
take mbb ; :: thesis:
thus mbb in dom V by A82; :: thesis:
thus L . a < L . (V /. mbb) by A76, A82, A83, PARTFUN1:def 6; :: thesis:
thus a <> V /. mbb by A76, A82, A83, PARTFUN1:def 6; :: thesis:
thus v,V /. mbb are_adjacent by A78, A82, A83, PARTFUN1:def 6; :: thesis:
thus not a,V /. mbb are_adjacent by A79, A82, A83, PARTFUN1:def 6; :: thesis:

end;

A84: for k being Nat st S₂[k] holds
k <= len V by FINSEQ_3:25;
consider mb being Nat such that
A85: S₂[mb] and
for n being Nat st S₂[n] holds
n <= mb from NAT_1:sch 6(A84, A81);
reconsider v = v, a = a, b = V /. mb as Vertex of G ;
consider ma being object such that
A86: ma in dom V and
A87: a = V . ma by A80, FUNCT_1:def 3;
reconsider ma = ma as Element of NAT by A86;
A88: a = V /. ma by A86, A87, PARTFUN1:def 6;
0 + 1 <= k by NAT_1:13;
then A89: k in dom V by A60, FINSEQ_3:25;

A90: now :: thesis:

assume ma <= k ; :: thesis:
then A91: ma < k by A62, A78, A79, A87, XXREAL_0:1;
a in the_Vertices_of G ;
then A92: a in rng V by CHORD:def 12;
V is one-to-one by CHORD:def 12;
then a .. V >= k by A75, A89, A92, CHORD:16;
then a .. V > ma by A91, XXREAL_0:2;
hence contradiction by A86, A87, FINSEQ_4:24; :: thesis:

end;

A93: v = V /. k by A62, A89, PARTFUN1:def 6;
then A94: L . v < L . a by A5, A89, A86, A88, A90;
A95: v <> b by A77, A85;
A96: S₁[4]

proof

A97: L . a > L . v by A5, A89, A93, A86, A88, A90;
consider c being Vertex of G such that
c in dom L and
A98: L . b < L . c and
A99: c,a are_adjacent and
A100: not c,v are_adjacent and
A101: 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, A85, A94;
consider P being Path of G, e1, e2 being object such that
A102: P is open and
A103: len P = 5 and
A104: P .length() = 2 and
e1 Joins b,v,G and
e2 Joins v,a,G and
P .edges() = {e1,e2} and
A105: P .vertices() = {b,v,a} and
A106: P . 1 = b and
A107: P . 3 = v and
A108: P . 5 = a by A77, A85, A95, CHORD:47;
consider e being object such that
A109: e Joins P .last() ,c,G by A99, A103, A108, CHORD:def 3;
set Qr = P .addEdge e;
set Q = (P .addEdge e) .reverse() ;
A110: (P .addEdge e) .last() = c by A109, GLIB_001:63;
A111: len (P .addEdge e) = 5 + 2 by A103, A109, GLIB_001:64;
then A112: 1 in dom (P .addEdge e) by FINSEQ_3:25;
5 in dom P by A103, FINSEQ_3:25;
then A113: (P .addEdge e) . 5 = a by A108, A109, GLIB_001:65;
5 in dom (P .addEdge e) by A111, FINSEQ_3:25;
then A114: a = ((P .addEdge e) .reverse()) . ((7 - 5) + 1) by A111, A113, GLIB_001:24;
7 in dom (P .addEdge e) by A111, FINSEQ_3:25;
then c = ((P .addEdge e) .reverse()) . ((7 - 7) + 1) by A111, A110, GLIB_001:24;
then A115: c = ((P .addEdge e) .reverse()) .first() ;
3 in dom P by A103, FINSEQ_3:25;
then A116: (P .addEdge e) . 3 = v by A107, A109, GLIB_001:65;
(P .addEdge e) .length() = 2 + 1 by A104, A109, Lm4;
then A117: ((P .addEdge e) .reverse()) .length() = (3 + 1) - 1 by Lm5;
1 in dom P by A103, FINSEQ_3:25;
then (P .addEdge e) . 1 = b by A106, A109, GLIB_001:65;
then b = ((P .addEdge e) .reverse()) . (((len (P .addEdge e)) - 1) + 1) by A112, GLIB_001:24;
then A118: b = ((P .addEdge e) .reverse()) .last() by GLIB_001:21;
A119: len ((P .addEdge e) .reverse()) = len (P .addEdge e) by GLIB_001:21;
A120: P .first() = b by A106;
P .last() = a by A103, A108;
then A121: P is chordless by A85, A103, A120, CHORD:90;

A122: now :: thesis:

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

per cases by A105, A123, ENUMSET1:def 1;

suppose x = b ; :: thesis:

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

end;

suppose x = v ; :: thesis:

hence L . x <= L . b by A85, A94, XXREAL_0:2; :: thesis:

end;

suppose x = a ; :: thesis:

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

end;

then A124: not c in P .vertices() by A98;
A125: for e being object holds not e Joins P . ((len P) - 2),c,G by A100, A103, A107, CHORD:def 3;
then P .addEdge e is open by A102, A121, A109, A124, CHORD:97;
then A126: (P .addEdge e) .reverse() is open by GLIB_001:120;

A127: now :: thesis:

let x be set ; :: thesis:
assume x in ((P .addEdge e) .reverse()) .vertices() ; :: thesis:
then x in (P .addEdge e) .vertices() by GLIB_001:92;
then A128: x in (P .vertices()) \/ {c} by A109, GLIB_001:95;

per cases by A128, XBOOLE_0:def 3;

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

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

end;

suppose x in {c} ; :: thesis:

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

end;

3 in dom (P .addEdge e) by A111, FINSEQ_3:25;
then v = ((P .addEdge e) .reverse()) . ((7 - 3) + 1) by A111, A116, GLIB_001:24;
then A129: v = ((P .addEdge e) .reverse()) . ((len ((P .addEdge e) .reverse())) - 2) by A111, A119;
P .addEdge e is chordless by A102, A121, A109, A124, A125, CHORD:97;
then A130: (P .addEdge e) .reverse() is chordless by CHORD:91;
P .addEdge e is Path-like by A102, A121, A109, A124, A125, CHORD:97;
hence S₁[4] by A85, A98, A101, A126, A130, A117, A114, A129, A118, A115, A97, A127; :: thesis:

end;

for i being Nat st 4 <= i holds
S₁[i] from NAT_1:sch 8(A96, A12);
then S₁[(G .order()) + 11] by A59, XXREAL_0:2;
then consider P being Walk of G, v1, v2, v3, v4 being Vertex of G such that
A131: P is Path-like and
P is open and
P is chordless and
A132: P .length() = ((G .order()) + 11) - 1 and
v1 = P . ((len P) - 2) and
v2 = P . 3 and
v3 = P .last() and
v4 = P .first() and
L . v4 > L . v3 and
L . v3 > L . v2 and
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 A132, GLIB_001:112;
then ((2 * (G .order())) + 21) + 1 = 2 * (len (P .vertexSeq())) by GLIB_001:def 14;
then (G .order()) + 11 <= (G .order()) + 1 by A131, GLIB_001:154;
hence contradiction by XREAL_1:8; :: thesis: