let G2 be _finite _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 .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 .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 .size() = (G2 .size()) + 1
let G1 be addEdge of G2,v1,e,v2; :: thesis: ( not e in the_Edges_of G2 implies G1 .size() = (G2 .size()) + 1 )
assume A1: not e in the_Edges_of G2 ; :: thesis: G1 .size() = (G2 .size()) + 1
then A2: the_Edges_of G1 = (the_Edges_of G2) \/ {e} by Def11;
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:40, ZFMISC_1:50
.= (G2 .size()) + (card {e}) by GLIB_000:def 25
.= (G2 .size()) + 1 by CARD_2:42 ; :: thesis: verum