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

hereby :: thesis: ( V is chordless implies W is chordless )

assume A2: W is chordless ; :: thesis: not V is chordal
assume V is chordal ; :: thesis: contradiction
then consider m, n being odd Nat such that
A3: m + 2 < n and
A4: n <= len V and
A5: V . m <> V . n and
A6: ex e being object st e Joins V . m,V . n,H and
A7: for f being object st f in V .edges() holds
not f Joins V . m,V . n,H ;
consider e being object such that
A8: e Joins V . m,V . n,H by A6;
n in NAT by ORDINAL1:def 12;
then V . n in V .vertices() by A4, GLIB_001:87;
then V . n in the_Vertices_of H ;
then A9: V . n in S by GLIB_000:def 37;
m + 0 <= m + 2 by XREAL_1:7;
then m <= n by A3, XXREAL_0:2;
then A10: m <= len V by A4, XXREAL_0:2;
m in NAT by ORDINAL1:def 12;
then V . m in V .vertices() by A10, GLIB_001:87;
then V . m in the_Vertices_of H ;
then A11: V . m in S by GLIB_000:def 37;
A12: for f being object st f in W .edges() holds
not f Joins W . m,W . n,G

proof

let f be object ; :: thesis: ( f in W .edges() implies not f Joins W . m,W . n,G )
assume f in W .edges() ; :: thesis: not f Joins W . m,W . n,G
then A13: f in V .edges() by A1, GLIB_001:110;
assume f Joins W . m,W . n,G ; :: thesis: contradiction
hence contradiction by A1, A7, A9, A11, A13, Th19; :: thesis: verum

end;

e Joins W . m,W . n,G by A1, A8, GLIB_000:72;
hence contradiction by A1, A2, A3, A4, A5, A12; :: thesis: verum

end;

assume A14: V is chordless ; :: thesis: W is chordless
assume W is chordal ; :: thesis: contradiction
then consider m, n being odd Nat such that
A15: m + 2 < n and
A16: n <= len W and
A17: W . m <> W . n and
A18: ex e being object st e Joins W . m,W . n,G and
A19: for f being object st f in W .edges() holds
not f Joins W . m,W . n,G ;
consider e being object such that
A20: e Joins W . m,W . n,G by A18;
A21: for f being object st f in V .edges() holds
not f Joins V . m,V . n,H

proof

let f be object ; :: thesis: ( f in V .edges() implies not f Joins V . m,V . n,H )
assume f in V .edges() ; :: thesis: not f Joins V . m,V . n,H
then A22: f in W .edges() by A1, GLIB_001:110;
assume f Joins V . m,V . n,H ; :: thesis: contradiction
then f Joins W . m,W . n,G by A1, GLIB_000:72;
hence contradiction by A19, A22; :: thesis: verum

end;

n in NAT by ORDINAL1:def 12;
then W . n in V .vertices() by A1, A16, GLIB_001:87;
then W . n in the_Vertices_of H ;
then A23: W . n in S by GLIB_000:def 37;
m + 0 <= m + 2 by XREAL_1:7;
then m <= n by A15, XXREAL_0:2;
then A24: m <= len W by A16, XXREAL_0:2;
m in NAT by ORDINAL1:def 12;
then W . m in V .vertices() by A1, A24, GLIB_001:87;
then W . m in the_Vertices_of H ;
then W . m in S by GLIB_000:def 37;
then e Joins V . m,V . n,H by A1, A20, A23, Th19;
hence contradiction by A1, A14, A15, A16, A17, A21; :: thesis: verum