let G be _Graph; 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; 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 ; ( 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 )
; 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 A7:
(
W1 . n = x &
W1 . (n + 2) = y )
;
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
;
( 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;
verum end;