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