let G be _Graph; :: thesis: for W1 being Walk of G
for e, x, y being object st e Joins x,y,G & e in W1 .edges() & W1 is Cycle-like holds
ex W2 being Path of G st
( W2 is_Walk_from x,y & W2 .edges() = (W1 .edges()) \ {e} & ( not e in G .loops() implies W2 is open ) )
let W1 be Walk of G; :: thesis: for e, x, y being object st e Joins x,y,G & e in W1 .edges() & W1 is Cycle-like holds
ex W2 being Path of G st
( W2 is_Walk_from x,y & W2 .edges() = (W1 .edges()) \ {e} & ( not e in G .loops() implies W2 is open ) )
let e, x, y be object ; :: thesis: ( e Joins x,y,G & e in W1 .edges() & W1 is Cycle-like implies ex W2 being Path of G st
( W2 is_Walk_from x,y & W2 .edges() = (W1 .edges()) \ {e} & ( not e in G .loops() implies W2 is open ) ) )
assume A1: ( e Joins x,y,G & e in W1 .edges() & W1 is Cycle-like ) ; :: thesis: ex W2 being Path of G st
( W2 is_Walk_from x,y & W2 .edges() = (W1 .edges()) \ {e} & ( not e in G .loops() implies W2 is open ) )
then consider n being odd Element of NAT such that
A2: ( n < len W1 & W1 . (n + 1) = e ) by GLIB_001:100;
set W7 = W1 .cut ((n + 2),(len W1));
set W8 = W1 .cut (1,n);
set W9 = (W1 .cut ((n + 2),(len W1))) .append (W1 .cut (1,n));
A3: (W1 .cut ((n + 2),(len W1))) .append (W1 .cut (1,n)) is_Walk_from W1 . (n + 2),W1 . n by A1, A2, Th31;
A4: ((W1 .cut ((n + 2),(len W1))) .append (W1 .cut (1,n))) .edges() = (W1 .edges()) \ {e} by A1, A2, Th31;
A5: ( (W1 .cut ((n + 2),(len W1))) .append (W1 .cut (1,n)) is Path-like & ( not e in G .loops() implies (W1 .cut ((n + 2),(len W1))) .append (W1 .cut (1,n)) is open ) ) by A1, A2, Th31;
W1 . (n + 1) Joins W1 . n,W1 . (n + 2),G by A2, GLIB_001:def 3;

per cases then ( ( W1 . n = y & W1 . (n + 2) = x ) or ( W1 . n = x & W1 . (n + 2) = y ) ) by A1, A2, GLIB_000:15;

suppose A6: ( W1 . n = y & W1 . (n + 2) = x ) ; :: thesis: ex W2 being Path of G st
( W2 is_Walk_from x,y & W2 .edges() = (W1 .edges()) \ {e} & ( not e in G .loops() implies W2 is open ) )

reconsider W2 = (W1 .cut ((n + 2),(len W1))) .append (W1 .cut (1,n)) as Path of G by A5;
take W2 ; :: thesis: ( W2 is_Walk_from x,y & W2 .edges() = (W1 .edges()) \ {e} & ( not e in G .loops() implies W2 is open ) )
thus ( W2 is_Walk_from x,y & W2 .edges() = (W1 .edges()) \ {e} & ( not e in G .loops() implies W2 is open ) ) by A3, A4, A5, A6; :: thesis: verum

end;

suppose A7: ( W1 . n = x & W1 . (n + 2) = y ) ; :: thesis: ex W2 being Path of G st
( W2 is_Walk_from x,y & W2 .edges() = (W1 .edges()) \ {e} & ( not e in G .loops() implies W2 is open ) )

reconsider W2 = ((W1 .cut ((n + 2),(len W1))) .append (W1 .cut (1,n))) .reverse() as Path of G by A5;
take W2 ; :: thesis: ( W2 is_Walk_from x,y & W2 .edges() = (W1 .edges()) \ {e} & ( not e in G .loops() implies W2 is open ) )
A8: W2 is_Walk_from x,y by A3, A7, GLIB_001:23;
W2 .edges() = (W1 .edges()) \ {e} by A4, GLIB_001:107;
hence ( W2 is_Walk_from x,y & W2 .edges() = (W1 .edges()) \ {e} & ( not e in G .loops() implies W2 is open ) ) by A5, A8, GLIB_001:120; :: thesis: verum

end;

end;