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

now

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 39;
hence H is chordal by Th95; :: 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 39;

now

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
A4: W is Path-like by A3;
reconsider P = W as Walk of G by GLIB_001:168;
reconsider P = P as Path of G by A4, GLIB_001:176;
( W is closed & not W is trivial & W is Path-like ) by A3;
then A5: ( P is closed & not P is trivial & P is Path-like ) by GLIB_001:177;
then A6: P is Cycle-like by GLIB_001:def 31;
P .length() > 3 by A2, GLIB_001:115;
then P is chordal by A6, Def11;
then consider m, n being odd Nat such that
A7: ( m + 2 < n & n <= len P ) and
P . m <> P . n and
A8: ( ex e being set st e Joins P . m,P . n,G & ( 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 Th84;
A9: ( m in NAT & n in NAT ) by ORDINAL1:def 13;
consider e being set such that
A10: e Joins P . m,P . n,G by A8;
m + 0 <= m + 2 by XREAL_1:9;
then m <= n by A7, XXREAL_0:2;
then ( P . m in the_Vertices_of H & P . n in the_Vertices_of H ) by A7, A9, GLIB_001:8, XXREAL_0:2;
then e Joins P . m,W . n,H by A1, A10, Th19;
hence W is chordal by A4, A5, A7, A8, Th85, GLIB_001:def 31; :: thesis: verum

end;

hence H is chordal by Def11; :: thesis: verum

end;

end;

end;

hence H is chordal ; :: thesis: verum