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 A3, GLIB_001:112;
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 A2, Th83;
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 A1, A6, A8, XXREAL_0:1;
then A13: n <= 9 - 2 by A4, Th3;
n <> 7 by A10, A9, A12;
then n < (2 * 3) + 1 by A13, XXREAL_0:1;
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 A1, A6, A8, XXREAL_0:1;
then n <= 9 - 2 by A4, Th3;
then n < jj by A1, A4, A8, A15, XXREAL_0:1;
then A16: n <= jj - 2 by Th3;
n <> 5 by A10, A9, A15;
then n < (2 * 2) + 1 by A16, XXREAL_0:1;
then n <= 5 - 2 by Th3;
hence contradiction by A5, A15; :: thesis: verum

end;

A17: W .first() = W .last() by A1, GLIB_001:def 24;

A18: now :: thesis: not m = 5

assume A19: m = 5 ; :: thesis: contradiction
n <> 9 by A17, A4, A9, A19, GLIB_000:14, A10;
then n < len W by A4, A6, XXREAL_0:1;
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 A14, XXREAL_0:1;
then 1 + 2 <= m by Th4;
then (2 * 1) + 1 < m by A11, XXREAL_0:1;
then 3 + 2 <= m by Th4;
then (2 * 2) + 1 < m by A18, XXREAL_0:1;
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