let G2 be _finite _Graph; 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; 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 ; 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; ( not e in the_Edges_of G2 implies G1 .size() = (G2 .size()) + 1 )
assume A1:
not e in the_Edges_of G2
; 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
; verum