let G2 be _Graph; :: thesis: for V being set
for G1 being addVertices of G2,V holds
( G2 is chordal iff G1 is chordal )
let V be set ; :: thesis: for G1 being addVertices of G2,V holds
( G2 is chordal iff G1 is chordal )
let G1 be addVertices of G2,V; :: thesis: ( G2 is chordal iff G1 is chordal )
thus ( G2 is chordal implies G1 is chordal ) :: thesis: ( G1 is chordal implies G2 is chordal )

proof

assume A1: G2 is chordal ; :: thesis: G1 is chordal
for P being Walk of G1 st P .length() > 3 & P is Cycle-like holds
P is chordal

proof

let P be Walk of G1; :: thesis: ( P .length() > 3 & P is Cycle-like implies P is chordal )
assume A2: ( P .length() > 3 & P is Cycle-like ) ; :: thesis: P is chordal

per cases ( P .vertices() misses V \ (the_Vertices_of G2) or not P is trivial ) by Th94;

suppose P .vertices() misses V \ (the_Vertices_of G2) ; :: thesis: P is chordal

then reconsider W = P as Walk of G2 by Th95;
A3: W is Cycle-like by A2, Th80;
P .length() = W .length() by GLIB_001:114;
then W is chordal by A1, A2, A3, CHORD:def 11;
then consider m, n being odd Nat such that
A4: ( m + 2 < n & n <= len W & W . m <> W . n ) and
A5: ex e being object st e Joins W . m,W . n,G2 and
A6: for f being object st f in W .edges() holds
not f Joins W . m,W . n,G2 by CHORD:def 10;

now :: thesis: ex m, n being odd Nat st
( m + 2 < n & n <= len P & P . m <> P . n & ex e being object st e Joins P . m,P . n,G1 & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G1 ) )

take m = m; :: thesis: ex n being odd Nat st
( m + 2 < n & n <= len P & P . m <> P . n & ex e being object st e Joins P . m,P . n,G1 & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G1 ) )
take n = n; :: thesis: ( m + 2 < n & n <= len P & P . m <> P . n & ex e being object st e Joins P . m,P . n,G1 & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G1 ) )
thus ( m + 2 < n & n <= len P & P . m <> P . n ) by A4; :: thesis: ( ex e being object st e Joins P . m,P . n,G1 & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G1 ) )
thus ex e being object st e Joins P . m,P . n,G1 by A5, Th74; :: thesis: for f being object st f in P .edges() holds
not f Joins P . m,P . n,G1
thus for f being object st f in P .edges() holds
not f Joins P . m,P . n,G1 :: thesis: verum

proof

given f being object such that A7: f in P .edges() and
A8: f Joins P . m,P . n,G1 ; :: thesis: contradiction
A9: f in W .edges() by A7, GLIB_001:110;

per cases ( f DJoins P . m,P . n,G1 or f DJoins P . n,P . m,G1 ) by A8, GLIB_000:16;

suppose f DJoins P . m,P . n,G1 ; :: thesis: contradiction

per cases then ( f DJoins P . m,P . n,G2 or not f in the_Edges_of G2 ) by Th75;

suppose f DJoins P . m,P . n,G2 ; :: thesis: contradiction

then f Joins W . m,W . n,G2 by GLIB_000:16;
hence contradiction by A6, A9; :: thesis: verum

end;

suppose not f in the_Edges_of G2 ; :: thesis: contradiction

hence contradiction by A9; :: thesis: verum

end;

end;

end;

suppose f DJoins P . n,P . m,G1 ; :: thesis: contradiction

per cases then ( f DJoins P . n,P . m,G2 or not f in the_Edges_of G2 ) by Th75;

suppose f DJoins P . n,P . m,G2 ; :: thesis: contradiction

then f Joins W . m,W . n,G2 by GLIB_000:16;
hence contradiction by A6, A9; :: thesis: verum

end;

suppose not f in the_Edges_of G2 ; :: thesis: contradiction

hence contradiction by A9; :: thesis: verum

end;

end;

end;

end;

end;

end;

hence P is chordal by CHORD:def 10; :: thesis: verum

end;

suppose P is trivial ; :: thesis: P is chordal

hence P is chordal by A2; :: thesis: verum

end;

end;

end;

hence G1 is chordal by CHORD:def 11; :: thesis: verum

end;

assume A10: G1 is chordal ; :: thesis: G2 is chordal
G2 is inducedSubgraph of G1,(the_Vertices_of G2) by Th88;
hence G2 is chordal by A10; :: thesis: verum