let G2 be _Graph; :: thesis: for V being set
for G1 being addVertices of G2,V holds
( G1 .size() = G2 .size() & G1 .order() = (G2 .order()) +` (card (V \ (the_Vertices_of G2))) )
let V be set ; :: thesis: for G1 being addVertices of G2,V holds
( G1 .size() = G2 .size() & G1 .order() = (G2 .order()) +` (card (V \ (the_Vertices_of G2))) )
let G1 be addVertices of G2,V; :: thesis: ( G1 .size() = G2 .size() & G1 .order() = (G2 .order()) +` (card (V \ (the_Vertices_of G2))) )
thus G1 .size() = card (the_Edges_of G1) by GLIB_000:def 25
.= card (the_Edges_of G2) by Def10
.= G2 .size() by GLIB_000:def 25 ; :: thesis: G1 .order() = (G2 .order()) +` (card (V \ (the_Vertices_of G2)))
thus G1 .order() = card (the_Vertices_of G1) by GLIB_000:def 24
.= card ((the_Vertices_of G2) \/ V) by Def10
.= card ((the_Vertices_of G2) \/ (V \ (the_Vertices_of G2))) by XBOOLE_1:39
.= (card (the_Vertices_of G2)) +` (card (V \ (the_Vertices_of G2))) by XBOOLE_1:79, CARD_2:35
.= (G2 .order()) +` (card (V \ (the_Vertices_of G2))) by GLIB_000:def 24 ; :: thesis: verum