let G1 be _finite non _trivial _Graph; :: thesis: for v being Vertex of G1
for G2 being removeVertex of G1,v holds
( (G2 .order()) + 1 = G1 .order() & (G2 .size()) + (card (v .edgesInOut())) = G1 .size() )
let v be Vertex of G1; :: thesis: for G2 being removeVertex of G1,v holds
( (G2 .order()) + 1 = G1 .order() & (G2 .size()) + (card (v .edgesInOut())) = G1 .size() )
let G2 be removeVertex of G1,v; :: thesis: ( (G2 .order()) + 1 = G1 .order() & (G2 .size()) + (card (v .edgesInOut())) = 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;
set EV = v .edgesInOut() ;
A1: the_Vertices_of G2 = (the_Vertices_of G1) \ {v} by Th47;
v in {v} by TARSKI:def 1;
then not v in the_Vertices_of G2 by A1, XBOOLE_0:def 5;
then card (((the_Vertices_of G1) \ {v}) \/ {v}) = (G2 .order()) + 1 by A1, CARD_2:41;
hence (G2 .order()) + 1 = G1 .order() by XBOOLE_1:45; :: thesis: (G2 .size()) + (card (v .edgesInOut())) = G1 .size()
A2: ( the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ {v}) & G1 .edgesBetween ((the_Vertices_of G1) \ {v}) = (the_Edges_of G1) \ (v .edgesInOut()) ) by Th35, Th47;
then the_Edges_of G1 = (the_Edges_of G2) \/ (v .edgesInOut()) by XBOOLE_1:45;
hence (G2 .size()) + (card (v .edgesInOut())) = G1 .size() by A2, CARD_2:40, XBOOLE_1:79; :: thesis: verum