let G be _Graph; :: thesis: for W being Walk of G st len W = 5 & not W .first() ,W .last() are_adjacent holds
W is chordless
let W be Walk of G; :: thesis: ( len W = 5 & not W .first() ,W .last() are_adjacent implies W is chordless )
assume that
A1: len W = 5 and
A2: not W .first() ,W .last() are_adjacent ; :: thesis: W is chordless
assume W is chordal ; :: thesis: contradiction
then consider m, n being odd Nat such that
A3: m + 2 < n and
A4: n <= len W and
W . m <> W . n and
A5: ex e being object st e Joins W . m,W . n,G and
( W is Cycle-like implies ( ( not m = 1 or not n = len W ) & ( not m = 1 or not n = (len W) - 2 ) & ( not m = 3 or not n = len W ) ) ) by Th83;

A6: now :: thesis: not m <> 1

assume A7: m <> 1 ; :: thesis: contradiction
1 <= m by Th2;
then (2 * 0) + 1 < m by A7, XXREAL_0:1;
then 1 + 2 <= m by Th4;
then 3 + 2 <= m + 2 by XREAL_1:7;
hence contradiction by A1, A3, A4, XXREAL_0:2; :: thesis: verum

end;

then 3 + 2 <= n by A3, Th4;
then W . n = W .last() by A1, A4, XXREAL_0:1;
hence contradiction by A2, A5, A6; :: thesis: verum