let G1, G2 be _Graph; :: thesis: ( G1 == G2 implies for W1 being Walk of G1

for W2 being Walk of G2 st W1 = W2 & W1 is chordal holds

W2 is chordal )

assume A1: G1 == G2 ; :: thesis: for W1 being Walk of G1

for W2 being Walk of G2 st W1 = W2 & W1 is chordal holds

W2 is chordal

let W1 be Walk of G1; :: thesis: for W2 being Walk of G2 st W1 = W2 & W1 is chordal holds

W2 is chordal

let W2 be Walk of G2; :: thesis: ( W1 = W2 & W1 is chordal implies W2 is chordal )

assume A2: W1 = W2 ; :: thesis: ( not W1 is chordal or W2 is chordal )

given m, n being odd Nat such that A3: m + 2 < n and

A4: n <= len W1 and

A5: W1 . m <> W1 . n and

A6: ex e being object st e Joins W1 . m,W1 . n,G1 and

A7: for f being object st f in W1 .edges() holds

not f Joins W1 . m,W1 . n,G1 ; :: 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,G2 & ( for f being object st f in W2 .edges() holds

not f Joins W2 . m,W2 . n,G2 ) )

take n ; :: thesis: ( m + 2 < n & n <= len W2 & W2 . m <> W2 . n & ex e being object st e Joins W2 . m,W2 . n,G2 & ( for f being object st f in W2 .edges() holds

not f Joins W2 . m,W2 . n,G2 ) )

thus ( m + 2 < n & n <= len W2 & W2 . m <> W2 . n ) by A2, A3, A4, A5; :: thesis: ( ex e being object st e Joins W2 . m,W2 . n,G2 & ( for f being object st f in W2 .edges() holds

not f Joins W2 . m,W2 . n,G2 ) )

consider e being object such that

A8: e Joins W1 . m,W1 . n,G1 by A6;

e Joins W2 . m,W2 . n,G2 by A1, A2, A8;

hence ex e being object st e Joins W2 . m,W2 . n,G2 ; :: thesis: for f being object st f in W2 .edges() holds

not f Joins W2 . m,W2 . n,G2

let f be object ; :: thesis: ( f in W2 .edges() implies not f Joins W2 . m,W2 . n,G2 )

assume f in W2 .edges() ; :: thesis: not f Joins W2 . m,W2 . n,G2

then f in W1 .edges() by A2, GLIB_001:110;

then not f Joins W1 . m,W1 . n,G1 by A7;

hence not f Joins W2 . m,W2 . n,G2 by A1, A2; :: thesis: verum

for W2 being Walk of G2 st W1 = W2 & W1 is chordal holds

W2 is chordal )

assume A1: G1 == G2 ; :: thesis: for W1 being Walk of G1

for W2 being Walk of G2 st W1 = W2 & W1 is chordal holds

W2 is chordal

let W1 be Walk of G1; :: thesis: for W2 being Walk of G2 st W1 = W2 & W1 is chordal holds

W2 is chordal

let W2 be Walk of G2; :: thesis: ( W1 = W2 & W1 is chordal implies W2 is chordal )

assume A2: W1 = W2 ; :: thesis: ( not W1 is chordal or W2 is chordal )

given m, n being odd Nat such that A3: m + 2 < n and

A4: n <= len W1 and

A5: W1 . m <> W1 . n and

A6: ex e being object st e Joins W1 . m,W1 . n,G1 and

A7: for f being object st f in W1 .edges() holds

not f Joins W1 . m,W1 . n,G1 ; :: 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,G2 & ( for f being object st f in W2 .edges() holds

not f Joins W2 . m,W2 . n,G2 ) )

take n ; :: thesis: ( m + 2 < n & n <= len W2 & W2 . m <> W2 . n & ex e being object st e Joins W2 . m,W2 . n,G2 & ( for f being object st f in W2 .edges() holds

not f Joins W2 . m,W2 . n,G2 ) )

thus ( m + 2 < n & n <= len W2 & W2 . m <> W2 . n ) by A2, A3, A4, A5; :: thesis: ( ex e being object st e Joins W2 . m,W2 . n,G2 & ( for f being object st f in W2 .edges() holds

not f Joins W2 . m,W2 . n,G2 ) )

consider e being object such that

A8: e Joins W1 . m,W1 . n,G1 by A6;

e Joins W2 . m,W2 . n,G2 by A1, A2, A8;

hence ex e being object st e Joins W2 . m,W2 . n,G2 ; :: thesis: for f being object st f in W2 .edges() holds

not f Joins W2 . m,W2 . n,G2

let f be object ; :: thesis: ( f in W2 .edges() implies not f Joins W2 . m,W2 . n,G2 )

assume f in W2 .edges() ; :: thesis: not f Joins W2 . m,W2 . n,G2

then f in W1 .edges() by A2, GLIB_001:110;

then not f Joins W1 . m,W1 . n,G1 by A7;

hence not f Joins W2 . m,W2 . n,G2 by A1, A2; :: thesis: verum