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: W .reverse() is chordal

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 A1, XXREAL_0:2;

then reconsider um = ((len W) - m) + 1, un = ((len W) - n) + 1 as odd Element of NAT by A2, FINSEQ_5:1, XXREAL_0:2;

reconsider um = um, un = un as odd Nat ;

A8: un + 2 < um by A1, Lm1;

1 <= n by Th2;

then n in dom W by A2, FINSEQ_3:25;

then A9: W . n = (W .reverse()) . un by GLIB_001:24;

A10: 1 <= m by Th2;

((len W) - m) + 1 <= len W by INT_1:7, XREAL_1:44;

then A11: um <= len (W .reverse()) by GLIB_001:21;

m <= len W by A2, A7, XXREAL_0:2;

then m in dom W by A10, FINSEQ_3:25;

then A12: W . m = (W .reverse()) . um by GLIB_001:24;

then A13: e Joins (W .reverse()) . un,(W .reverse()) . um,G by A6, A9;

W .edges() = (W .reverse()) .edges() by GLIB_001:107;

then for f being object st f in (W .reverse()) .edges() holds

not f Joins (W .reverse()) . un,(W .reverse()) . um,G by A5, A12, A9, GLIB_000:14;

hence W .reverse() is chordal by A3, A8, A11, A12, A9, A13; :: thesis: verum

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: W .reverse() is chordal

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 A1, XXREAL_0:2;

then reconsider um = ((len W) - m) + 1, un = ((len W) - n) + 1 as odd Element of NAT by A2, FINSEQ_5:1, XXREAL_0:2;

reconsider um = um, un = un as odd Nat ;

A8: un + 2 < um by A1, Lm1;

1 <= n by Th2;

then n in dom W by A2, FINSEQ_3:25;

then A9: W . n = (W .reverse()) . un by GLIB_001:24;

A10: 1 <= m by Th2;

((len W) - m) + 1 <= len W by INT_1:7, XREAL_1:44;

then A11: um <= len (W .reverse()) by GLIB_001:21;

m <= len W by A2, A7, XXREAL_0:2;

then m in dom W by A10, FINSEQ_3:25;

then A12: W . m = (W .reverse()) . um by GLIB_001:24;

then A13: e Joins (W .reverse()) . un,(W .reverse()) . um,G by A6, A9;

W .edges() = (W .reverse()) .edges() by GLIB_001:107;

then for f being object st f in (W .reverse()) .edges() holds

not f Joins (W .reverse()) . un,(W .reverse()) . um,G by A5, A12, A9, GLIB_000:14;

hence W .reverse() is chordal by A3, A8, A11, A12, A9, A13; :: thesis: verum