let G2 be _finite _Graph; :: thesis: for v being object
for V being finite set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
G1 .size() = (G2 .size()) + (card V)
let v be object ; :: thesis: for V being finite set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
G1 .size() = (G2 .size()) + (card V)
let V be finite set ; :: thesis: for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
G1 .size() = (G2 .size()) + (card V)
let G1 be addAdjVertexAll of G2,v,V; :: thesis: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 implies G1 .size() = (G2 .size()) + (card V) )
assume A1: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) ; :: thesis: G1 .size() = (G2 .size()) + (card V)
consider E being set such that
A2: card V = card E and
A3: ( E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E ) and
for w being object st w in V holds
ex e1 being object st
( e1 in E & e1 Joins w,v,G1 & ( for e2 being object st e2 Joins w,v,G1 holds
e1 = e2 ) ) by A1, Def4;
V,E are_equipotent by A2, CARD_1:5;
then reconsider E = E as finite set by CARD_1:38;
thus G1 .size() = card (the_Edges_of G1) by GLIB_000:def 25
.= (card (the_Edges_of G2)) + (card E) by A3, CARD_2:40
.= (G2 .size()) + (card V) by A2, GLIB_000:def 25 ; :: thesis: verum