let G1 be _finite _Graph; :: thesis: for e being set
for G2 being removeEdge of G1,e holds G1 .numComponents() c= G2 .numComponents()
let e be set ; :: thesis: for G2 being removeEdge of G1,e holds G1 .numComponents() c= G2 .numComponents()
let G2 be removeEdge of G1,e; :: thesis: 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 ; :: thesis: 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 ; :: thesis: 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; :: thesis: verum

end;

suppose A9: v2 in G2 .reachableFrom v1 ; :: thesis: G1 .numComponents() c= G2 .numComponents()

G1 .numComponents() = card (G1 .componentSet()) by GLIB_002:def 9
.= card (G2 .componentSet()) by A9, Th40
.= G2 .numComponents() by GLIB_002:def 9 ;
hence G1 .numComponents() c= G2 .numComponents() ; :: thesis: verum

end;

end;

end;

suppose not e in the_Edges_of G1 ; :: thesis: G1 .numComponents() c= G2 .numComponents()

then (the_Edges_of G1) \ {e} = the_Edges_of G1 by ZFMISC_1:57
.= G1 .edgesBetween (the_Vertices_of G1) by GLIB_000:34 ;
hence G1 .numComponents() c= G2 .numComponents() by GLIB_002:29, GLIB_000:94; :: thesis: verum

end;

end;