let G be _Graph; for W being Walk of G st W is chordal holds
W .reverse() is chordal
let W be Walk of G; ( W is chordal implies W .reverse() is chordal )
set U = W .reverse() ;
assume
W is chordal
; 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; verum