let G be _Graph; :: thesis: for S being non empty Subset of (the_Vertices_of G)
for H being inducedSubgraph of G,S
for W1 being Walk of G
for W2 being Walk of H st W1 = W2 holds
( W2 is chordal iff W1 is chordal )
let S be non empty Subset of (the_Vertices_of G); :: thesis: for H being inducedSubgraph of G,S
for W1 being Walk of G
for W2 being Walk of H st W1 = W2 holds
( W2 is chordal iff W1 is chordal )
let H be inducedSubgraph of G,S; :: thesis: for W1 being Walk of G
for W2 being Walk of H st W1 = W2 holds
( W2 is chordal iff W1 is chordal )
let W1 be Walk of G; :: thesis: for W2 being Walk of H st W1 = W2 holds
( W2 is chordal iff W1 is chordal )
let W2 be Walk of H; :: thesis: ( W1 = W2 implies ( W2 is chordal iff W1 is chordal ) )
assume A1: W1 = W2 ; :: thesis: ( W2 is chordal iff W1 is chordal )
thus ( W2 is chordal implies W1 is chordal ) :: thesis: ( W1 is chordal implies W2 is chordal )

proof

given m, n being odd Nat such that A2: m + 2 < n and
A3: n <= len W2 and
A4: W2 . m <> W2 . n and
A5: ex e being object st e Joins W2 . m,W2 . n,H and
A6: for f being object st f in W2 .edges() holds
not f Joins W2 . m,W2 . n,H ; :: according to CHORD:def 10 :: thesis: W1 is chordal
take m ; :: according to CHORD:def 10 :: thesis: ex n being odd Nat st
( m + 2 < n & n <= len W1 & W1 . m <> W1 . n & ex e being object st e Joins W1 . m,W1 . n,G & ( for f being object st f in W1 .edges() holds
not f Joins W1 . m,W1 . n,G ) )
take n ; :: thesis: ( m + 2 < n & n <= len W1 & W1 . m <> W1 . n & ex e being object st e Joins W1 . m,W1 . n,G & ( for f being object st f in W1 .edges() holds
not f Joins W1 . m,W1 . n,G ) )
thus ( m + 2 < n & n <= len W1 & W1 . m <> W1 . n ) by A1, A2, A3, A4; :: thesis: ( ex e being object st e Joins W1 . m,W1 . n,G & ( for f being object st f in W1 .edges() holds
not f Joins W1 . m,W1 . n,G ) )
consider e being object such that
A7: e Joins W2 . m,W2 . n,H by A5;
e Joins W1 . m,W1 . n,G by A1, A7, GLIB_000:72;
hence ex e being object st e Joins W1 . m,W1 . n,G ; :: thesis: for f being object st f in W1 .edges() holds
not f Joins W1 . m,W1 . n,G
let f be object ; :: thesis: ( f in W1 .edges() implies not f Joins W1 . m,W1 . n,G )
assume f in W1 .edges() ; :: thesis: not f Joins W1 . m,W1 . n,G
then A8: f in W2 .edges() by A1, GLIB_001:110;
then not f Joins W1 . m,W1 . n,H by A1, A6;
hence not f Joins W1 . m,W1 . n,G by A8, GLIB_000:73; :: thesis: verum

end;

A9: S = the_Vertices_of H by GLIB_000:def 37;
thus ( W1 is chordal implies W2 is chordal ) :: thesis: verum

proof

given m, n being odd Nat such that A10: m + 2 < n and
A11: n <= len W1 and
A12: W1 . m <> W1 . n and
A13: ex e being object st e Joins W1 . m,W1 . n,G and
A14: for f being object st f in W1 .edges() holds
not f Joins W1 . m,W1 . n,G ; :: according to CHORD:def 10 :: thesis: W2 is chordal
take m ; :: according to CHORD:def 10 :: thesis: ex n being odd Nat st
( m + 2 < n & n <= len W2 & W2 . m <> W2 . n & ex e being object st e Joins W2 . m,W2 . n,H & ( for f being object st f in W2 .edges() holds
not f Joins W2 . m,W2 . n,H ) )
take n ; :: thesis: ( m + 2 < n & n <= len W2 & W2 . m <> W2 . n & ex e being object st e Joins W2 . m,W2 . n,H & ( for f being object st f in W2 .edges() holds
not f Joins W2 . m,W2 . n,H ) )
thus ( m + 2 < n & n <= len W2 & W2 . m <> W2 . n ) by A1, A10, A11, A12; :: thesis: ( ex e being object st e Joins W2 . m,W2 . n,H & ( for f being object st f in W2 .edges() holds
not f Joins W2 . m,W2 . n,H ) )
A15: m in NAT by ORDINAL1:def 12;
n in NAT by ORDINAL1:def 12;
then A16: W1 . n in the_Vertices_of H by A1, A11, GLIB_001:7;
m < n by A10, NAT_1:12;
then W1 . m in the_Vertices_of H by A1, A11, A15, GLIB_001:7, XXREAL_0:2;
hence ex e being object st e Joins W2 . m,W2 . n,H by A1, A9, A13, A16, Th19; :: thesis: for f being object st f in W2 .edges() holds
not f Joins W2 . m,W2 . n,H
let f be object ; :: thesis: ( f in W2 .edges() implies not f Joins W2 . m,W2 . n,H )
assume f in W2 .edges() ; :: thesis: not f Joins W2 . m,W2 . n,H
then f in W1 .edges() by A1, GLIB_001:110;
then not f Joins W2 . m,W2 . n,G by A1, A14;
hence not f Joins W2 . m,W2 . n,H by GLIB_000:72; :: thesis: verum

end;