let G2 be _Graph; :: thesis: for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 holds
( G1 .order() = G2 .order() & G1 .size() = (G2 .size()) +` 1 )
let v1, v2 be Vertex of G2; :: thesis: for e being object
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 holds
( G1 .order() = G2 .order() & G1 .size() = (G2 .size()) +` 1 )
let e be object ; :: thesis: for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 holds
( G1 .order() = G2 .order() & G1 .size() = (G2 .size()) +` 1 )
let G1 be addEdge of G2,v1,e,v2; :: thesis: ( not e in the_Edges_of G2 implies ( G1 .order() = G2 .order() & G1 .size() = (G2 .size()) +` 1 ) )
assume A1: not e in the_Edges_of G2 ; :: thesis: ( G1 .order() = G2 .order() & G1 .size() = (G2 .size()) +` 1 )
then A2: ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ {e} ) by Def11;
thus G1 .order() = card (the_Vertices_of G1) by GLIB_000:def 24
.= G2 .order() by A2, GLIB_000:def 24 ; :: 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 A1, A2, CARD_2:35, ZFMISC_1:50
.= (G2 .size()) +` (card {e}) by GLIB_000:def 25
.= (G2 .size()) +` 1 by CARD_2:42 ; :: thesis: verum