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