let G be _Graph; :: thesis: for W being Walk of G st W is Cycle-like & W is chordal & W .length() = 4 holds
ex e being object st
( e Joins W . 1,W . 5,G or e Joins W . 3,W . 7,G )

let W be Walk of G; :: thesis: ( W is Cycle-like & W is chordal & W .length() = 4 implies ex e being object st
( e Joins W . 1,W . 5,G or e Joins W . 3,W . 7,G ) )

assume that
A1: W is Cycle-like and
A2: W is chordal and
A3: W .length() = 4 ; :: thesis: ex e being object st
( e Joins W . 1,W . 5,G or e Joins W . 3,W . 7,G )

A4: len W = (2 * 4) + 1 by ;
consider m, n being odd Nat such that
A5: m + 2 < n and
A6: n <= len W and
W . m <> W . n and
A7: ex e being object st e Joins W . m,W . n,G and
A8: ( 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 ;
consider e being object such that
A9: e Joins W . m,W . n,G by A7;
assume A10: for e being object holds
( not e Joins W . 1,W . 5,G & not e Joins W . 3,W . 7,G ) ; :: thesis: contradiction
A11: now :: thesis: not m = 3
assume A12: m = 3 ; :: thesis: contradiction
then n < len W by ;
then A13: n <= 9 - 2 by ;
n <> 7 by A10, A9, A12;
then n < (2 * 3) + 1 by ;
then n <= 7 - 2 by Th3;
hence contradiction by A5, A12; :: thesis: verum
end;
A14: now :: thesis: not m = 1
reconsider jj = (2 * 3) + 1 as odd Nat ;
assume A15: m = 1 ; :: thesis: contradiction
then n < len W by ;
then n <= 9 - 2 by ;
then n < jj by ;
then A16: n <= jj - 2 by Th3;
n <> 5 by A10, A9, A15;
then n < (2 * 2) + 1 by ;
then n <= 5 - 2 by Th3;
hence contradiction by A5, A15; :: thesis: verum
end;
A17: W .first() = W .last() by ;
A18: now :: thesis: not m = 5
assume A19: m = 5 ; :: thesis: contradiction
n <> 9 by ;
then n < len W by ;
then n <= (len W) - 2 by Th3;
hence contradiction by A4, A5, A19; :: thesis: verum
end;
0 + 1 <= m by ABIAN:12;
then (2 * 0) + 1 < m by ;
then 1 + 2 <= m by Th4;
then (2 * 1) + 1 < m by ;
then 3 + 2 <= m by Th4;
then (2 * 2) + 1 < m by ;
then 5 + 2 <= m by Th4;
then 7 + 2 <= m + 2 by XREAL_1:7;
hence contradiction by A4, A5, A6, XXREAL_0:2; :: thesis: verum