let G be _Graph; :: thesis: for W being Walk of G holds

( W is chordal iff W .reverse() is chordal )

let W be Walk of G; :: thesis: ( W is chordal iff W .reverse() is chordal )

thus ( W is chordal implies W .reverse() is chordal ) by Lm3; :: thesis: ( W .reverse() is chordal implies W is chordal )

assume W .reverse() is chordal ; :: thesis: W is chordal

then (W .reverse()) .reverse() is chordal by Lm3;

hence W is chordal ; :: thesis: verum

( W is chordal iff W .reverse() is chordal )

let W be Walk of G; :: thesis: ( W is chordal iff W .reverse() is chordal )

thus ( W is chordal implies W .reverse() is chordal ) by Lm3; :: thesis: ( W .reverse() is chordal implies W is chordal )

assume W .reverse() is chordal ; :: thesis: W is chordal

then (W .reverse()) .reverse() is chordal by Lm3;

hence W is chordal ; :: thesis: verum