let G2 be _Graph; 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; 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 ; 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; ( 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 )
; ( 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:35
.=
(G2 .order()) +` (card {v2})
by GLIB_000:def 24
.=
(G2 .order()) +` 1
by CARD_2:42
; 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:35
.=
(G2 .size()) +` (card {e})
by GLIB_000:def 25
.=
(G2 .size()) +` 1
by CARD_2:42
; verum