let G be connected _Graph; for e being object st e in (the_Edges_of G) \ (G .loops()) holds
ex T being spanning Tree-like plain Subgraph of G st e in the_Edges_of T
let e be object ; ( e in (the_Edges_of G) \ (G .loops()) implies ex T being spanning Tree-like plain Subgraph of G st e in the_Edges_of T )
assume
e in (the_Edges_of G) \ (G .loops())
; ex T being spanning Tree-like plain Subgraph of G st e in the_Edges_of T
then A1:
( e in the_Edges_of G & not e in G .loops() )
by XBOOLE_0:def 5;
set T1 = the spanning Tree-like plain Subgraph of G;
per cases
( e in the_Edges_of the spanning Tree-like plain Subgraph of G or not e in the_Edges_of the spanning Tree-like plain Subgraph of G )
;
suppose A3:
not
e in the_Edges_of the
spanning Tree-like plain Subgraph of
G
;
ex T being spanning Tree-like plain Subgraph of G st e in the_Edges_of Tset v =
(the_Source_of G) . e;
set w =
(the_Target_of G) . e;
set G2 = the
addEdge of the
spanning Tree-like plain Subgraph of
G,
(the_Source_of G) . e,
e,
(the_Target_of G) . e;
e DJoins (the_Source_of G) . e,
(the_Target_of G) . e,
G
by A1, GLIB_000:def 14;
then reconsider G2 = the
addEdge of the
spanning Tree-like plain Subgraph of
G,
(the_Source_of G) . e,
e,
(the_Target_of G) . e as
Subgraph of
G by GLIBPRE1:50;
(
(the_Source_of G) . e is
Vertex of
G &
(the_Target_of G) . e is
Vertex of
G )
by A1, FUNCT_2:5;
then A4:
(
(the_Source_of G) . e is
Vertex of the
spanning Tree-like plain Subgraph of
G &
(the_Target_of G) . e is
Vertex of the
spanning Tree-like plain Subgraph of
G )
by GLIB_000:def 33;
then A5:
( not
G2 is
acyclic & ( for
W1,
W2 being
Walk of
G2 st
W1 is
Cycle-like &
W2 is
Cycle-like holds
W1 .edges() = W2 .edges() ) )
by A3, GLIBPRE1:51;
then consider W being
Walk of
G2 such that A6:
W is
Cycle-like
by GLIB_002:def 2;
A7:
e in W .edges()
G2 .loops() c= G .loops()
by GLIB_009:48;
then
not
e in G2 .loops()
by A1;
then consider e0 being
object such that A8:
(
e0 in W .edges() &
e0 <> e )
by A6, A7, GLIBPRE1:29;
reconsider e0 =
e0 as
set by TARSKI:1;
set T3 = the
plain removeEdge of
G2,
e0;
set w1 =
(the_Source_of G2) . e0;
set w2 =
(the_Target_of G2) . e0;
A9:
G2 is
addEdge of the
plain removeEdge of
G2,
e0,
(the_Source_of G2) . e0,
e0,
(the_Target_of G2) . e0
by A8, GLIB_008:37;
A10:
e0 Joins (the_Source_of G2) . e0,
(the_Target_of G2) . e0,
G2
by A8, GLIB_000:def 13;
e0 in {e0}
by TARSKI:def 1;
then
not
e0 in (the_Edges_of G2) \ {e0}
by XBOOLE_0:def 5;
then A11:
not
e0 in the_Edges_of the
plain removeEdge of
G2,
e0
by GLIB_000:51;
(
(the_Source_of G2) . e0 in the_Vertices_of G2 &
(the_Target_of G2) . e0 in the_Vertices_of G2 )
by A10, GLIB_000:13;
then A12:
(
(the_Source_of G2) . e0 is
Vertex of the
plain removeEdge of
G2,
e0 &
(the_Target_of G2) . e0 is
Vertex of the
plain removeEdge of
G2,
e0 )
by GLIB_000:def 33;
now for v1, v2 being Vertex of the plain removeEdge of G2,e0 ex W3 being Walk of the plain removeEdge of G2,e0 st W3 is_Walk_from v1,v2let v1,
v2 be
Vertex of the
plain removeEdge of
G2,
e0;
ex W3 being Walk of the plain removeEdge of G2,e0 st b3 is_Walk_from W3,b2reconsider u1 =
v1,
u2 =
v2 as
Vertex of
G2 by GLIB_000:def 33;
consider W2 being
Walk of
G2 such that A13:
W2 is_Walk_from u1,
u2
by GLIB_002:def 1;
set P2 = the
Path-like Subwalk of
W2;
A14:
the
Path-like Subwalk of
W2 is_Walk_from u1,
u2
by A13, GLIB_001:160;
per cases
( not e0 in the Path-like Subwalk of W2 .edges() or e0 in the Path-like Subwalk of W2 .edges() )
;
suppose A15:
e0 in the
Path-like Subwalk of
W2 .edges()
;
ex W3 being Walk of the plain removeEdge of G2,e0 st b3 is_Walk_from W3,b2consider P4 being
Path of
G2 such that A16:
(
P4 is_Walk_from (the_Source_of G2) . e0,
(the_Target_of G2) . e0 &
P4 .edges() = (W .edges()) \ {e0} )
and
( not
e0 in G2 .loops() implies
P4 is
open )
by A6, A8, A10, GLIBPRE1:32;
e0 in {e0}
by TARSKI:def 1;
then A17:
not
e0 in P4 .edges()
by A16, XBOOLE_0:def 5;
A18:
(
P4 .first() = (the_Source_of G2) . e0 &
P4 .last() = (the_Target_of G2) . e0 )
by A16, GLIB_001:def 23;
per cases
( G2 .walkOf (((the_Source_of G2) . e0),e0,((the_Target_of G2) . e0)) is_odd_substring_of the Path-like Subwalk of W2, 0 or G2 .walkOf (((the_Target_of G2) . e0),e0,((the_Source_of G2) . e0)) is_odd_substring_of the Path-like Subwalk of W2, 0 )
by A10, A15, GLIB_006:28;
suppose A19:
G2 .walkOf (
((the_Source_of G2) . e0),
e0,
((the_Target_of G2) . e0))
is_odd_substring_of the
Path-like Subwalk of
W2,
0
;
ex W3 being Walk of the plain removeEdge of G2,e0 st b3 is_Walk_from W3,b2set W4 = the
Path-like Subwalk of
W2 .replaceEdgeWith (
e0,
P4);
(
e0 Joins P4 .first() ,
P4 .last() ,
G2 &
G2 .walkOf (
(P4 .first()),
e0,
(P4 .last()))
is_odd_substring_of the
Path-like Subwalk of
W2,
0 )
by A10, A18, A19;
then
not
e0 in ( the Path-like Subwalk of W2 .replaceEdgeWith (e0,P4)) .edges()
by A17, GLIB_006:40;
then reconsider W3 = the
Path-like Subwalk of
W2 .replaceEdgeWith (
e0,
P4) as
Walk of the
plain removeEdge of
G2,
e0 by GLIB_001:172;
take W3 =
W3;
W3 is_Walk_from v1,v2
the
Path-like Subwalk of
W2 .replaceEdgeWith (
e0,
P4)
is_Walk_from u1,
u2
by A14, GLIB_006:47;
hence
W3 is_Walk_from v1,
v2
by GLIB_001:19;
verum end; suppose A20:
G2 .walkOf (
((the_Target_of G2) . e0),
e0,
((the_Source_of G2) . e0))
is_odd_substring_of the
Path-like Subwalk of
W2,
0
;
ex W3 being Walk of the plain removeEdge of G2,e0 st b3 is_Walk_from W3,b2set W4 = the
Path-like Subwalk of
W2 .replaceEdgeWith (
e0,
(P4 .reverse()));
A21:
not
e0 in (P4 .reverse()) .edges()
by A17, GLIB_001:107;
(
(P4 .reverse()) .first() = (the_Target_of G2) . e0 &
(P4 .reverse()) .last() = (the_Source_of G2) . e0 )
by A18, GLIB_001:22;
then
(
e0 Joins (P4 .reverse()) .first() ,
(P4 .reverse()) .last() ,
G2 &
G2 .walkOf (
((P4 .reverse()) .first()),
e0,
((P4 .reverse()) .last()))
is_odd_substring_of the
Path-like Subwalk of
W2,
0 )
by A10, A20, GLIB_000:14;
then
not
e0 in ( the Path-like Subwalk of W2 .replaceEdgeWith (e0,(P4 .reverse()))) .edges()
by A21, GLIB_006:40;
then reconsider W3 = the
Path-like Subwalk of
W2 .replaceEdgeWith (
e0,
(P4 .reverse())) as
Walk of the
plain removeEdge of
G2,
e0 by GLIB_001:172;
take W3 =
W3;
W3 is_Walk_from v1,v2
the
Path-like Subwalk of
W2 .replaceEdgeWith (
e0,
(P4 .reverse()))
is_Walk_from u1,
u2
by A14, GLIB_006:47;
hence
W3 is_Walk_from v1,
v2
by GLIB_001:19;
verum end; end; end; then
the
plain removeEdge of
G2,
e0 is
connected
by GLIB_002:def 1;
then A22:
the
plain removeEdge of
G2,
e0 is
Tree-like
by A5, A9, A11, A12, GLIBPRE1:52;
the_Vertices_of the
plain removeEdge of
G2,
e0 =
the_Vertices_of G2
by GLIB_000:def 33
.=
the_Vertices_of the
spanning Tree-like plain Subgraph of
G
by A4, GLIB_006:102
.=
the_Vertices_of G
by GLIB_000:def 33
;
then reconsider T3 = the
plain removeEdge of
G2,
e0 as
spanning Tree-like plain Subgraph of
G by A22, GLIB_000:def 33, GLIB_000:43;
take
T3
;
e in the_Edges_of T3
not
e in {e0}
by A8, TARSKI:def 1;
then
e in (the_Edges_of G2) \ {e0}
by A7, XBOOLE_0:def 5;
hence
e in the_Edges_of T3
by GLIB_000:51;
verum end;