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 () or V is non empty Subset of () ) ;
suppose V is non empty Subset of () ; :: 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 ;
A4: not P is trivial by ;
A5: P .length() > 3 by ;
A6: P is closed by ;
then P is Cycle-like by A4;
then P is chordal by ;
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 ;
n in NAT by ORDINAL1:def 12;
then A13: P . n in the_Vertices_of H by ;
m in NAT by ORDINAL1:def 12;
then P . m in the_Vertices_of H by ;
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;
hence H is chordal ; :: thesis: verum
end;
end;
end;
hence H is chordal ; :: thesis: verum