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 )

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

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

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 A14:
V is chordless
; :: thesis: 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

hence contradiction by A1, A2, A3, A4, A5, A12; :: thesis: verum

end;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

e Joins W . m,W . n,G
by A1, A8, GLIB_000:72;
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;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

hence contradiction by A1, A2, A3, A4, A5, A12; :: thesis: verum

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

n in NAT
by ORDINAL1:def 12;
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;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

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