let G2 be _Graph; :: thesis: for E being set
for G1 being reverseEdgeDirections of G2,E
for W2 being Walk of G2
for W1 being Walk of G1 st W1 = W2 & W1 is chordal holds
W2 is chordal
let E be set ; :: thesis: for G1 being reverseEdgeDirections of G2,E
for W2 being Walk of G2
for W1 being Walk of G1 st W1 = W2 & W1 is chordal holds
W2 is chordal
let G1 be reverseEdgeDirections of G2,E; :: thesis: for W2 being Walk of G2
for W1 being Walk of G1 st W1 = W2 & W1 is chordal holds
W2 is chordal
let W2 be Walk of G2; :: thesis: for W1 being Walk of G1 st W1 = W2 & W1 is chordal holds
W2 is chordal
let W1 be Walk of G1; :: thesis: ( W1 = W2 & W1 is chordal implies W2 is chordal )
assume A1: W1 = W2 ; :: thesis: ( not W1 is chordal or W2 is chordal )
assume W1 is chordal ; :: thesis: W2 is chordal
then consider m, n being odd Nat such that
A2: ( m + 2 < n & n <= len W1 & W1 . m <> W1 . n ) and
A3: ex e being object st e Joins W1 . m,W1 . n,G1 and
A4: for f being object st f in W1 .edges() holds
not f Joins W1 . m,W1 . n,G1 by CHORD:def 10;
ex k, l being odd Nat st
( k + 2 < l & l <= len W2 & W2 . k <> W2 . l & ex e being object st e Joins W2 . k,W2 . l,G2 & ( for f being object st f in W2 .edges() holds
not f Joins W2 . k,W2 . l,G2 ) )

proof

take m ; :: thesis: ex l being odd Nat st
( m + 2 < l & l <= len W2 & W2 . m <> W2 . l & ex e being object st e Joins W2 . m,W2 . l,G2 & ( for f being object st f in W2 .edges() holds
not f Joins W2 . m,W2 . l,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 A1, A2; :: 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 ) )
thus ex e being object st e Joins W2 . m,W2 . n,G2 by A1, A3, Th9; :: 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 A1, GLIB_001:110;
hence not f Joins W2 . m,W2 . n,G2 by A1, Th9, A4; :: thesis: verum

end;

hence W2 is chordal by CHORD:def 10; :: thesis: verum