let G be Tree-like _Graph; :: thesis: for v1, v2 being Vertex of G
for e being object
for H being addEdge of G,v1,e,v2 st not e in the_Edges_of G holds
( not H is acyclic & ( for W1, W2 being Walk of H st W1 is Cycle-like & W2 is Cycle-like holds
W1 .edges() = W2 .edges() ) )
let v1, v2 be Vertex of G; :: thesis: for e being object
for H being addEdge of G,v1,e,v2 st not e in the_Edges_of G holds
( not H is acyclic & ( for W1, W2 being Walk of H st W1 is Cycle-like & W2 is Cycle-like holds
W1 .edges() = W2 .edges() ) )
let e be object ; :: thesis: for H being addEdge of G,v1,e,v2 st not e in the_Edges_of G holds
( not H is acyclic & ( for W1, W2 being Walk of H st W1 is Cycle-like & W2 is Cycle-like holds
W1 .edges() = W2 .edges() ) )
let H be addEdge of G,v1,e,v2; :: thesis: ( not e in the_Edges_of G implies ( not H is acyclic & ( for W1, W2 being Walk of H st W1 is Cycle-like & W2 is Cycle-like holds
W1 .edges() = W2 .edges() ) ) )
assume A1: not e in the_Edges_of G ; :: thesis: ( not H is acyclic & ( for W1, W2 being Walk of H st W1 is Cycle-like & W2 is Cycle-like holds
W1 .edges() = W2 .edges() ) )
v2 in the_Vertices_of G ;
then v2 in G .reachableFrom v1 by GLIB_002:16;
hence not H is acyclic by A1, GLIB_006:119; :: thesis: for W1, W2 being Walk of H st W1 is Cycle-like & W2 is Cycle-like holds
W1 .edges() = W2 .edges()
let W1, W2 be Walk of H; :: thesis: ( W1 is Cycle-like & W2 is Cycle-like implies W1 .edges() = W2 .edges() )
assume A2: ( W1 is Cycle-like & W2 is Cycle-like ) ; :: thesis: W1 .edges() = W2 .edges()
A3: e in W1 .edges()
proof
assume not e in W1 .edges() ; :: thesis: contradiction
then reconsider W7 = W1 as Walk of G by GLIB_006:109;
W7 is Cycle-like by A2, GLIB_006:24;
hence contradiction by GLIB_002:def 2; :: thesis: verum
end;
A4: e in W2 .edges()
proof
assume not e in W2 .edges() ; :: thesis: contradiction
then reconsider W8 = W2 as Walk of G by GLIB_006:109;
W8 is Cycle-like by A2, GLIB_006:24;
hence contradiction by GLIB_002:def 2; :: thesis: verum
end;
e DJoins v1,v2,H by A1, GLIB_006:105;
then A5: e Joins v1,v2,H by GLIB_000:16;
consider W3 being Path of H such that
A6: ( W3 is_Walk_from v1,v2 & W3 .edges() = (W1 .edges()) \ {e} ) and
( not e in H .loops() implies W3 is open ) by A2, A3, A5, Th32;
consider W4 being Path of H such that
A7: ( W4 is_Walk_from v1,v2 & W4 .edges() = (W2 .edges()) \ {e} ) and
( not e in H .loops() implies W4 is open ) by A2, A4, A5, Th32;
e in {e} by TARSKI:def 1;
then A8: ( not e in W3 .edges() & not e in W4 .edges() ) by A6, A7, XBOOLE_0:def 5;
then reconsider W5 = W3 as Walk of G by GLIB_006:109;
reconsider W6 = W4 as Walk of G by A8, GLIB_006:109;
A9: ( W5 is_Walk_from v1,v2 & W5 is Path-like ) by A6, GLIB_001:19, GLIB_006:23;
A10: ( W6 is_Walk_from v1,v2 & W6 is Path-like ) by A7, GLIB_001:19, GLIB_006:23;
A11: W3 .edges() = (G .pathBetween (v1,v2)) .edges() by A9, HELLY:def 2, GLIB_001:110
.= W4 .edges() by A10, HELLY:def 2, GLIB_001:110 ;
thus W1 .edges() = (W3 .edges()) \/ {e} by A3, A6, ZFMISC_1:116
.= W2 .edges() by A4, A7, A11, ZFMISC_1:116 ; :: thesis: verum