let G2 be _finite _Graph; :: thesis: for v1, e being object
for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 holds
( G1 .order() = (G2 .order()) + 1 & G1 .size() = (G2 .size()) + 1 )
let v1, e be object ; :: thesis: for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 holds
( G1 .order() = (G2 .order()) + 1 & G1 .size() = (G2 .size()) + 1 )
let v2 be Vertex of G2; :: thesis: for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 holds
( G1 .order() = (G2 .order()) + 1 & G1 .size() = (G2 .size()) + 1 )
let G1 be addAdjVertex of G2,v1,e,v2; :: thesis: ( not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 implies ( G1 .order() = (G2 .order()) + 1 & G1 .size() = (G2 .size()) + 1 ) )
assume A1: ( not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 ) ; :: thesis: ( G1 .order() = (G2 .order()) + 1 & G1 .size() = (G2 .size()) + 1 )
then A2: ( the_Vertices_of G1 = (the_Vertices_of G2) \/ {v1} & the_Edges_of G1 = (the_Edges_of G2) \/ {e} ) by Def14;
A3: ( the_Vertices_of G2 misses {v1} & the_Edges_of G2 misses {e} ) by A1, ZFMISC_1:50;
thus G1 .order() = card (the_Vertices_of G1) by GLIB_000:def 24
.= (card (the_Vertices_of G2)) + (card {v1}) by A2, A3, CARD_2:40
.= (G2 .order()) + (card {v1}) by GLIB_000:def 24
.= (G2 .order()) + 1 by CARD_2:42 ; :: thesis: G1 .size() = (G2 .size()) + 1
thus G1 .size() = card (the_Edges_of G1) by GLIB_000:def 25
.= (card (the_Edges_of G2)) + (card {e}) by A2, A3, CARD_2:40
.= (G2 .size()) + (card {e}) by GLIB_000:def 25
.= (G2 .size()) + 1 by CARD_2:42 ; :: thesis: verum