reconsider n = (2 * 2) + 1 as odd Nat ;
reconsider m = (2 * 0) + 1 as odd Nat ;
let G be finite _Graph; :: thesis: ( ( for a, b being Vertex of G st a <> b & not a,b are_adjacent holds
for S being VertexSeparator of a,b st S is minimal & not S is empty holds
for G2 being inducedSubgraph of G,S holds G2 is complete ) implies G is chordal )

assume A1: for a, b being Vertex of G st a <> b & not a,b are_adjacent holds
for S being VertexSeparator of a,b st S is minimal & not S is empty holds
for G2 being inducedSubgraph of G,S holds G2 is complete ; :: thesis: G is chordal
let P be Walk of G; :: according to CHORD:def 11 :: thesis: ( P .length() > 3 & P is Cycle-like implies P is chordal )
assume that
A2: P .length() > 3 and
A3: P is Cycle-like ; :: thesis: P is chordal
P .length() >= 3 + 1 by ;
then 2 * () >= 2 * 4 by XREAL_1:64;
then (2 * ()) + 1 >= 8 + 1 by XREAL_1:7;
then A4: len P >= 9 by GLIB_001:112;
A5: now :: thesis: not P . m = P . n
assume A6: P . m = P . n ; :: thesis: contradiction
n <= len P by ;
then n = len P by ;
hence contradiction by A4; :: thesis: verum
end;
per cases ( ex e being object st e Joins P . m,P . n,G or for e being object holds not e Joins P . m,P . n,G ) ;
suppose A7: ex e being object st e Joins P . m,P . n,G ; :: thesis: P is chordal
A8: m + 2 < n ;
(len P) + (- 2) >= 9 + (- 2) by ;
then A9: ( not m = 1 or not n = (len P) - 2 ) ;
A10: ( not m = 1 or not n = len P ) by A4;
n <= len P by ;
hence P is chordal by A3, A7, A8, A10, A9, Th84; :: thesis: verum
end;
suppose A11: for e being object holds not e Joins P . m,P . n,G ; :: thesis: P is chordal
reconsider Pn = P . n as Vertex of G by ;
reconsider Pm = P . m as Vertex of G by ;
set P5l = P .cut (n,(len P));
consider S being VertexSeparator of Pm,Pn such that
A12: S is minimal by Th78;
set G2 = the inducedSubgraph of G,S;
A13: n <= len P by ;
then P .cut (n,(len P)) is_Walk_from P . n,P . (len P) by GLIB_001:37;
then A14: P .cut (n,(len P)) is_Walk_from P . n,P . m by ;
A15: not Pm,Pn are_adjacent by A11;
then S is VertexSeparator of Pn,Pm by ;
then consider l being odd Nat such that
A16: 1 < l and
A17: l < len (P .cut (n,(len P))) and
A18: (P .cut (n,(len P))) . l in S by A5, A15, A14, Th71;
A19: 1 + (- 1) < l + (- 1) by ;
then reconsider l2 = l - 1 as even Element of NAT by INT_1:3;
reconsider l2 = l2 as even Nat ;
A20: l + (- 1) < (len (P .cut (n,(len P)))) + (- 1) by ;
((len (P .cut (n,(len P)))) + 5) + (- 5) = ((len P) + 1) + (- 5) by ;
then A21: l2 + n < ((len P) - 5) + n by ;
l + (- 1) < l + 0 by XREAL_1:8;
then l - 1 < len (P .cut (n,(len P))) by ;
then (P .cut (n,(len P))) . (l2 + 1) = P . (n + l2) by ;
then reconsider bb = P . (n + l2) as Vertex of the inducedSubgraph of G,S by ;
set P15 = P .cut (m,n);
A22: n <= len P by ;
then A23: P .cut (m,n) is_Walk_from P . m,P . n by GLIB_001:37;
then not S is empty by ;
then A24: the inducedSubgraph of G,S is complete by A1, A5, A15, A12;
A25: ((len (P .cut (m,n))) + 1) + (- 1) = (5 + 1) + (- 1) by ;
then consider k being odd Nat such that
A26: m < k and
A27: k < n and
A28: (P .cut (m,n)) . k in S by A5, A15, A23, Th71;
A29: k <= 5 - 2 by ;
A30: 1 + 2 <= k by ;
then A31: k = 3 by ;
(P .cut (m,n)) . (2 + 1) = P . (1 + 2) by ;
then P . 3 in S by ;
then reconsider aa = P . 3 as Vertex of the inducedSubgraph of G,S by GLIB_000:def 37;
A32: (k + 2) + 0 < (k + 2) + l2 by ;
A33: n + l2 in NAT by ORDINAL1:def 12;
now :: thesis: not aa = bb
assume A34: aa = bb ; :: thesis: contradiction
k < n + l2 by ;
hence contradiction by A3, A31, A21, A33, A34, GLIB_001:def 28; :: thesis: verum
end;
then aa,bb are_adjacent by A24;
then consider e being object such that
A35: e Joins P . 3,P . (n + l2), the inducedSubgraph of G,S ;
e Joins P . k,P . (n + l2),G by ;
hence P is chordal by A3, A31, A21, A32, Th84; :: thesis: verum
end;
end;