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

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

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;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

A14: now :: thesis: not m = 1

A17:
W .first() = W .last()
by A1, GLIB_001:def 24;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;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

A18: now :: thesis: not m = 5

0 + 1 <= m
by ABIAN:12;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;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

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