let G be _Graph; :: thesis: for W being Walk of G st W is chordal holds
W .reverse() is chordal

let W be Walk of G; :: thesis: ( W is chordal implies W .reverse() is chordal )
set U = W .reverse() ;
assume W is chordal ; :: thesis:
then consider m, n being odd Nat such that
A1: m + 2 < n and
A2: n <= len W and
A3: W . m <> W . n and
A4: ex e being object st e Joins W . m,W . n,G and
A5: for f being object st f in W .edges() holds
not f Joins W . m,W . n,G ;
consider e being object such that
A6: e Joins W . m,W . n,G by A4;
set um = ((len W) - m) + 1;
set un = ((len W) - n) + 1;
m < m + 2 by XREAL_1:29;
then A7: m < n by ;
then reconsider um = ((len W) - m) + 1, un = ((len W) - n) + 1 as odd Element of NAT by ;
reconsider um = um, un = un as odd Nat ;
A8: un + 2 < um by ;
1 <= n by Th2;
then n in dom W by ;
then A9: W . n = () . un by GLIB_001:24;
A10: 1 <= m by Th2;
((len W) - m) + 1 <= len W by ;
then A11: um <= len () by GLIB_001:21;
m <= len W by ;
then m in dom W by ;
then A12: W . m = () . um by GLIB_001:24;
then A13: e Joins () . un,() . um,G by A6, A9;
W .edges() = () .edges() by GLIB_001:107;
then for f being object st f in () .edges() holds
not f Joins () . un,() . um,G by ;
hence W .reverse() is chordal by A3, A8, A11, A12, A9, A13; :: thesis: verum