let G1 be _finite _Graph; :: thesis: for V being Subset of (the_Vertices_of G1)
for G2 being removeVertices of G1,V st V <> the_Vertices_of G1 holds
( (G2 .order()) + (card V) = G1 .order() & (G2 .size()) + (card (G1 .edgesInOut V)) = G1 .size() )
let V be Subset of (the_Vertices_of G1); :: thesis: for G2 being removeVertices of G1,V st V <> the_Vertices_of G1 holds
( (G2 .order()) + (card V) = G1 .order() & (G2 .size()) + (card (G1 .edgesInOut V)) = G1 .size() )
let G2 be removeVertices of G1,V; :: thesis: ( V <> the_Vertices_of G1 implies ( (G2 .order()) + (card V) = G1 .order() & (G2 .size()) + (card (G1 .edgesInOut V)) = G1 .size() ) )
set VG1 = the_Vertices_of G1;
set VG2 = the_Vertices_of G2;
set EG1 = the_Edges_of G1;
set EG2 = the_Edges_of G2;
A1: G1 .edgesBetween ((the_Vertices_of G1) \ V) = (the_Edges_of G1) \ (G1 .edgesInOut V) by Th35;
assume V <> the_Vertices_of G1 ; :: thesis: ( (G2 .order()) + (card V) = G1 .order() & (G2 .size()) + (card (G1 .edgesInOut V)) = G1 .size() )
then A2: V c< the_Vertices_of G1 by XBOOLE_0:def 8;
then A3: the_Vertices_of G2 = (the_Vertices_of G1) \ V by Th49;
then card ((the_Vertices_of G2) \/ V) = (card (the_Vertices_of G2)) + (card V) by CARD_2:40, XBOOLE_1:79;
hence (G2 .order()) + (card V) = G1 .order() by A3, XBOOLE_1:45; :: thesis: (G2 .size()) + (card (G1 .edgesInOut V)) = G1 .size()
A4: the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ V) by A2, Th49;
then the_Edges_of G1 = (the_Edges_of G2) \/ (G1 .edgesInOut V) by A1, XBOOLE_1:45;
hence (G2 .size()) + (card (G1 .edgesInOut V)) = G1 .size() by A4, A1, CARD_2:40, XBOOLE_1:79; :: thesis: verum