let H be inducedSubgraph of G,V; :: thesis: H is chordal

now :: thesis: H is chordal end;

hence
H is chordal
; :: thesis: verumper cases
( not V is non empty Subset of (the_Vertices_of G) or V is non empty Subset of (the_Vertices_of G) )
;

end;

suppose
V is non empty Subset of (the_Vertices_of G)
; :: thesis: H is chordal

then A1:
V = the_Vertices_of H
by GLIB_000:def 37;

end;now :: thesis: for W being Walk of H st W .length() > 3 & W is Cycle-like holds

W is chordal

hence
H is chordal
; :: thesis: verumW is chordal

let W be Walk of H; :: thesis: ( W .length() > 3 & W is Cycle-like implies W is chordal )

assume that

A2: W .length() > 3 and

A3: W is Cycle-like ; :: thesis: W is chordal

reconsider P = W as Walk of G by GLIB_001:167;

reconsider P = P as Path of G by A3, GLIB_001:175;

A4: not P is trivial by A3, GLIB_001:176;

A5: P .length() > 3 by A2, GLIB_001:114;

A6: P is closed by A3, GLIB_001:176;

then P is Cycle-like by A4;

then P is chordal by A5, Def11;

then consider m, n being odd Nat such that

A7: m + 2 < n and

A8: n <= len P and

P . m <> P . n and

A9: ex e being object st e Joins P . m,P . n,G and

A10: ( P is Cycle-like implies ( ( not m = 1 or not n = len P ) & ( not m = 1 or not n = (len P) - 2 ) & ( not m = 3 or not n = len P ) ) ) by Th83;

consider e being object such that

A11: e Joins P . m,P . n,G by A9;

m + 0 <= m + 2 by XREAL_1:7;

then A12: m <= n by A7, XXREAL_0:2;

n in NAT by ORDINAL1:def 12;

then A13: P . n in the_Vertices_of H by A8, GLIB_001:7;

m in NAT by ORDINAL1:def 12;

then P . m in the_Vertices_of H by A8, A12, GLIB_001:7, XXREAL_0:2;

then e Joins P . m,W . n,H by A1, A11, A13, Th19;

hence W is chordal by A3, A6, A4, A7, A8, A10, Th84; :: thesis: verum

end;assume that

A2: W .length() > 3 and

A3: W is Cycle-like ; :: thesis: W is chordal

reconsider P = W as Walk of G by GLIB_001:167;

reconsider P = P as Path of G by A3, GLIB_001:175;

A4: not P is trivial by A3, GLIB_001:176;

A5: P .length() > 3 by A2, GLIB_001:114;

A6: P is closed by A3, GLIB_001:176;

then P is Cycle-like by A4;

then P is chordal by A5, Def11;

then consider m, n being odd Nat such that

A7: m + 2 < n and

A8: n <= len P and

P . m <> P . n and

A9: ex e being object st e Joins P . m,P . n,G and

A10: ( P is Cycle-like implies ( ( not m = 1 or not n = len P ) & ( not m = 1 or not n = (len P) - 2 ) & ( not m = 3 or not n = len P ) ) ) by Th83;

consider e being object such that

A11: e Joins P . m,P . n,G by A9;

m + 0 <= m + 2 by XREAL_1:7;

then A12: m <= n by A7, XXREAL_0:2;

n in NAT by ORDINAL1:def 12;

then A13: P . n in the_Vertices_of H by A8, GLIB_001:7;

m in NAT by ORDINAL1:def 12;

then P . m in the_Vertices_of H by A8, A12, GLIB_001:7, XXREAL_0:2;

then e Joins P . m,W . n,H by A1, A11, A13, Th19;

hence W is chordal by A3, A6, A4, A7, A8, A10, Th84; :: thesis: verum