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 set 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 set st
( e Joins W . 1,W . 5,G or e Joins W . 3,W . 7,G ) )
assume that
A1: ( W is Cycle-like & W is chordal ) and
A2: W .length() = 4 ; :: thesis: ex e being set st
( e Joins W . 1,W . 5,G or e Joins W . 3,W . 7,G )
W is closed by A1;
then A3: W .first() = W .last() by GLIB_001:def 24;
A4: len W = (2 * 4) + 1 by A2, GLIB_001:113;
assume A5: for e being set holds
( not e Joins W . 1,W . 5,G & not e Joins W . 3,W . 7,G ) ; :: thesis: contradiction
consider m, n being odd Nat such that
A6: ( m + 2 < n & n <= len W & W . m <> W . n & ex e being set st e Joins W . m,W . n,G & ( 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 A1, Th84;
consider e being set such that
A7: e Joins W . m,W . n,G by A6;
A8: 0 + 1 <= m by HEYTING3:1;

now

assume A9: m = 1 ; :: thesis: contradiction
then n < len W by A1, A6, XXREAL_0:1;
then A10: n <= 9 - 2 by A4, Th3;
reconsider jj = (2 * 3) + 1 as odd Nat ;
n < jj by A1, A4, A6, A9, A10, XXREAL_0:1;
then A11: n <= jj - 2 by Th3;
n <> 5 by A5, A7, A9;
then n < (2 * 2) + 1 by A11, XXREAL_0:1;
then n <= 5 - 2 by Th3;
hence contradiction by A6, A9; :: thesis: verum

end;

then (2 * 0 ) + 1 < m by A8, XXREAL_0:1;
then A12: 1 + 2 <= m by Th4;

now

assume A13: m = 3 ; :: thesis: contradiction
then n < len W by A1, A6, XXREAL_0:1;
then A14: n <= 9 - 2 by A4, Th3;
n <> 7 by A5, A7, A13;
then n < (2 * 3) + 1 by A14, XXREAL_0:1;
then n <= 7 - 2 by Th3;
hence contradiction by A6, A13; :: thesis: verum

end;

then (2 * 1) + 1 < m by A12, XXREAL_0:1;
then A15: 3 + 2 <= m by Th4;

now

assume A16: m = 5 ; :: thesis: contradiction

now

assume n = 9 ; :: thesis: contradiction
then e Joins W . 1,W . 5,G by A3, A4, A7, A16, GLIB_000:17;
hence contradiction by A5; :: thesis: verum

end;

then n < len W by A4, A6, XXREAL_0:1;
then n <= (len W) - 2 by Th3;
hence contradiction by A4, A6, A16; :: thesis: verum

end;

then (2 * 2) + 1 < m by A15, XXREAL_0:1;
then 5 + 2 <= m by Th4;
then 7 + 2 <= m + 2 by XREAL_1:9;
hence contradiction by A4, A6, XXREAL_0:2; :: thesis: verum