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;

then W . n = W .last() by A1, A4, XXREAL_0:1;

hence contradiction by A2, A5, A6; :: thesis: verum

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

then
3 + 2 <= n
by A3, Th4;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;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

then W . n = W .last() by A1, A4, XXREAL_0:1;

hence contradiction by A2, A5, A6; :: thesis: verum