let G1 be _finite _Graph; for e being set
for G2 being removeEdge of G1,e holds G1 .numComponents() c= G2 .numComponents()
let e be set ; for G2 being removeEdge of G1,e holds G1 .numComponents() c= G2 .numComponents()
let G2 be removeEdge of G1,e; G1 .numComponents() c= G2 .numComponents()
per cases
( e in the_Edges_of G1 or not e in the_Edges_of G1 )
;
suppose A1:
e in the_Edges_of G1
;
G1 .numComponents() c= G2 .numComponents() set w1 =
(the_Source_of G1) . e;
set w2 =
(the_Target_of G1) . e;
reconsider w1 =
(the_Source_of G1) . e,
w2 =
(the_Target_of G1) . e as
Vertex of
G1 by A1, FUNCT_2:5;
A2:
G1 is
addEdge of
G2,
w1,
e,
w2
by A1, Th37;
reconsider v1 =
w1,
v2 =
w2 as
Vertex of
G2 by GLIB_000:51;
reconsider G1 =
G1 as
addEdge of
G2,
v1,
e,
v2 by A2;
A3:
the_Edges_of G2 = (the_Edges_of G1) \ {e}
by GLIB_000:51;
e in {e}
by TARSKI:def 1;
then A4:
not
e in the_Edges_of G2
by A3, XBOOLE_0:def 5;
set V1 =
G2 .reachableFrom v1;
set V2 =
G2 .reachableFrom v2;
per cases
( not v2 in G2 .reachableFrom v1 or v2 in G2 .reachableFrom v1 )
;
suppose A5:
not
v2 in G2 .reachableFrom v1
;
G1 .numComponents() c= G2 .numComponents() then
not
(G2 .reachableFrom v1) \/ (G2 .reachableFrom v2) in G2 .componentSet()
by Lm7;
then A6:
not
(G2 .reachableFrom v1) \/ (G2 .reachableFrom v2) in (G2 .componentSet()) \ {(G2 .reachableFrom v1),(G2 .reachableFrom v2)}
by XBOOLE_1:36, TARSKI:def 3;
(
G2 .reachableFrom v1 in G2 .componentSet() &
G2 .reachableFrom v2 in G2 .componentSet() )
by GLIB_002:def 8;
then A7:
{(G2 .reachableFrom v1),(G2 .reachableFrom v2)} c= G2 .componentSet()
by ZFMISC_1:32;
A8:
G2 .reachableFrom v1 <> G2 .reachableFrom v2
by A5, Th22;
G1 .numComponents() =
card (G1 .componentSet())
by GLIB_002:def 9
.=
card (((G2 .componentSet()) \ {(G2 .reachableFrom v1),(G2 .reachableFrom v2)}) \/ {((G2 .reachableFrom v1) \/ (G2 .reachableFrom v2))})
by A4, Th44
.=
(card ((G2 .componentSet()) \ {(G2 .reachableFrom v1),(G2 .reachableFrom v2)})) + 1
by A6, CARD_2:41
.=
((card (G2 .componentSet())) - (card {(G2 .reachableFrom v1),(G2 .reachableFrom v2)})) + 1
by A7, CARD_2:44
.=
((card (G2 .componentSet())) - 2) + 1
by A8, CARD_2:57
.=
((G2 .numComponents()) - 2) + 1
by GLIB_002:def 9
.=
(G2 .numComponents()) - 1
;
then
G2 .numComponents() = (G1 .numComponents()) +` 1
;
hence
G1 .numComponents() c= G2 .numComponents()
by CARD_2:94;
verum end; end; end; end;