let G2 be _finite _Graph; :: thesis: for v1 being Vertex of G2
for e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 holds
( G1 .order() = (G2 .order()) + 1 & G1 .size() = (G2 .size()) + 1 )
let v1 be Vertex of G2; :: thesis: for e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 holds
( G1 .order() = (G2 .order()) + 1 & G1 .size() = (G2 .size()) + 1 )
let e, v2 be object ; :: thesis: for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v2 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 v2 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 v2 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) \/ {v2} & the_Edges_of G1 = (the_Edges_of G2) \/ {e} ) by Def13;
A3: ( the_Vertices_of G2 misses {v2} & 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 {v2}) by A2, A3, CARD_2:40
.= (G2 .order()) + (card {v2}) 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