let G be _Graph; :: thesis: for S being non empty Subset of ()
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 (); :: 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 ;
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 ;
then not f Joins W1 . m,W1 . n,H by A1, A6;
hence not f Joins W1 . m,W1 . n,G by ; :: 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 ;
m < n by ;
then W1 . m in the_Vertices_of H by ;
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 ;
then not f Joins W2 . m,W2 . n,G by ;
hence not f Joins W2 . m,W2 . n,H by GLIB_000:72; :: thesis: verum
end;