let G2 be _Graph; :: thesis: for v being object
for V being 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 .order() = (G2 .order()) +` 1 & G1 .size() = (G2 .size()) +` (card V) )
let v be object ; :: thesis: for V being 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 .order() = (G2 .order()) +` 1 & G1 .size() = (G2 .size()) +` (card V) )
let V be 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 .order() = (G2 .order()) +` 1 & 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 .order() = (G2 .order()) +` 1 & G1 .size() = (G2 .size()) +` (card V) ) )
assume A1: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) ; :: thesis: ( G1 .order() = (G2 .order()) +` 1 & G1 .size() = (G2 .size()) +` (card V) )
then A2: the_Vertices_of G1 = (the_Vertices_of G2) \/ {v} by Def4;
consider E being set such that
A3: card V = card E and
A4: ( 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;
A5: {v} misses the_Vertices_of G2 by A1, ZFMISC_1:50;
thus G1 .order() = card (the_Vertices_of G1) by GLIB_000:def 24
.= (card (the_Vertices_of G2)) +` (card {v}) by A2, A5, CARD_2:35
.= (G2 .order()) +` (card {v}) by GLIB_000:def 24
.= (G2 .order()) +` 1 by CARD_1:30 ; :: thesis: G1 .size() = (G2 .size()) +` (card V)
thus G1 .size() = card (the_Edges_of G1) by GLIB_000:def 25
.= (card (the_Edges_of G2)) +` (card E) by A4, CARD_2:35
.= (G2 .size()) +` (card V) by A3, GLIB_000:def 25 ; :: thesis: verum