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

now :: thesis: H is chordal

per cases ( not V is non empty Subset of (the_Vertices_of G) or V is non empty Subset of (the_Vertices_of G) ) ;

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

then H == G by GLIB_000:def 37;
hence H is chordal by Th94; :: thesis: verum

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;

now :: thesis: for W being Walk of H st W .length() > 3 & W is Cycle-like holds
W 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: P is trivial by A3;
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, A7, A8, A10, Th84; :: thesis: verum

end;

hence H is chordal ; :: thesis: verum

end;

end;

end;

hence H is chordal ; :: thesis: verum