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 )

thus ( W1 is chordal implies W2 is chordal ) :: thesis: verum

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

A9:
S = the_Vertices_of H
by GLIB_000:def 37;
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;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

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