let G be _Graph; :: thesis: for W1 being Walk of G
for e, x, y being set st e Joins x,y,G & e in W1 .edges() & W1 is Cycle-like holds
ex W2 being Walk of G st
( W2 is_Walk_from x,y & not e in W2 .edges() )

let W1 be Walk of G; :: thesis: for e, x, y being set st e Joins x,y,G & e in W1 .edges() & W1 is Cycle-like holds
ex W2 being Walk of G st
( W2 is_Walk_from x,y & not e in W2 .edges() )

let e, x, y be set ; :: thesis: ( e Joins x,y,G & e in W1 .edges() & W1 is Cycle-like implies ex W2 being Walk of G st
( W2 is_Walk_from x,y & not e in W2 .edges() ) )

assume that
A1: e Joins x,y,G and
A2: e in W1 .edges() and
A3: W1 is Cycle-like ; :: thesis: ex W2 being Walk of G st
( W2 is_Walk_from x,y & not e in W2 .edges() )

consider v1, v2 being Vertex of G, n being odd Element of NAT such that
A4: n + 2 <= len W1 and
A5: v1 = W1 . n and
A6: e = W1 . (n + 1) and
A7: v2 = W1 . (n + 2) and
A8: e Joins v1,v2,G by ;
set WA = W1 .cut ((n + 2),(len W1));
set WB = W1 .cut (((2 * 0) + 1),n);
A9: (W1 .cut ((n + 2),(len W1))) .last() = W1 .last() by ;
A10: (n + 2) - 2 < (len W1) - 0 by ;
A11: now :: thesis: not e in (W1 .cut (((2 * 0) + 1),n)) .edges()
assume e in (W1 .cut (((2 * 0) + 1),n)) .edges() ; :: thesis: contradiction
then consider m being even Element of NAT such that
A12: 1 <= m and
A13: m <= len (W1 .cut (((2 * 0) + 1),n)) and
A14: (W1 .cut (((2 * 0) + 1),n)) . m = e by Lm46;
m in dom (W1 .cut (((2 * 0) + 1),n)) by ;
then A15: W1 . m = W1 . (n + 1) by A6, A10, A14, Lm23;
len (W1 .cut (((2 * 0) + 1),n)) = n by ;
then A16: m + 0 < n + 1 by ;
n + 1 <= len W1 by ;
hence contradiction by A3, A12, A15, A16, Lm57; :: thesis: verum
end;
1 <= n by ABIAN:12;
then W1 .cut (((2 * 0) + 1),n) is_Walk_from W1 .first() ,v1 by ;
then A17: W1 .cut (((2 * 0) + 1),n) is_Walk_from W1 .last() ,v1 by ;
A18: W1 .cut ((n + 2),(len W1)) is_Walk_from v2,W1 . (len W1) by A4, A7, Lm16;
then (W1 .cut ((n + 2),(len W1))) .append (W1 .cut (((2 * 0) + 1),n)) is_Walk_from v2,v1 by ;
then A19: ((W1 .cut ((n + 2),(len W1))) .append (W1 .cut (((2 * 0) + 1),n))) .reverse() is_Walk_from v1,v2 by Th22;
A20: now :: thesis: not e in (W1 .cut ((n + 2),(len W1))) .edges()
assume e in (W1 .cut ((n + 2),(len W1))) .edges() ; :: thesis: contradiction
then consider m being even Element of NAT such that
A21: 1 <= m and
A22: m <= len (W1 .cut ((n + 2),(len W1))) and
A23: (W1 .cut ((n + 2),(len W1))) . m = e by Lm46;
reconsider maa1 = m - 1 as odd Element of NAT by ;
A24: maa1 < (len (W1 .cut ((n + 2),(len W1)))) - 0 by ;
then (n + 2) + maa1 in dom W1 by ;
then A25: (n + 2) + maa1 <= len W1 by FINSEQ_3:25;
maa1 + 1 = m ;
then A26: e = W1 . ((n + 2) + maa1) by A4, A23, A24, Lm15;
n + 1 < (n + 1) + 1 by NAT_1:13;
then A27: (n + 1) + 0 < (n + 2) + maa1 by XREAL_1:8;
1 <= n + 1 by NAT_1:12;
hence contradiction by A3, A6, A26, A25, A27, Lm57; :: thesis: verum
end;
(W1 .cut (((2 * 0) + 1),n)) .first() = W1 .last() by A17;
then ((W1 .cut ((n + 2),(len W1))) .append (W1 .cut (((2 * 0) + 1),n))) .edges() = ((W1 .cut ((n + 2),(len W1))) .edges()) \/ ((W1 .cut (((2 * 0) + 1),n)) .edges()) by ;
then A28: not e in ((W1 .cut ((n + 2),(len W1))) .append (W1 .cut (((2 * 0) + 1),n))) .edges() by ;
then A29: not e in (((W1 .cut ((n + 2),(len W1))) .append (W1 .cut (((2 * 0) + 1),n))) .reverse()) .edges() by Th105;
now :: thesis: ex W2 being Walk of G st
( W2 is_Walk_from x,y & not e in W2 .edges() )
per cases ( ( x = v1 & y = v2 ) or ( x = v2 & y = v1 ) ) by ;
suppose ( x = v1 & y = v2 ) ; :: thesis: ex W2 being Walk of G st
( W2 is_Walk_from x,y & not e in W2 .edges() )

hence ex W2 being Walk of G st
( W2 is_Walk_from x,y & not e in W2 .edges() ) by ; :: thesis: verum
end;
suppose ( x = v2 & y = v1 ) ; :: thesis: ex W2 being Walk of G st
( W2 is_Walk_from x,y & not e in W2 .edges() )

hence ex W2 being Walk of G st
( W2 is_Walk_from x,y & not e in W2 .edges() ) by ; :: thesis: verum
end;
end;
end;
hence ex W2 being Walk of G st
( W2 is_Walk_from x,y & not e in W2 .edges() ) ; :: thesis: verum