let G2 be _finite _Graph; :: thesis: for V being finite set
for G1 being addVertices of G2,V holds G1 .order() = (G2 .order()) + (card (V \ (the_Vertices_of G2)))
let V be finite set ; :: thesis: for G1 being addVertices of G2,V holds G1 .order() = (G2 .order()) + (card (V \ (the_Vertices_of G2)))
let G1 be addVertices of G2,V; :: 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:40
.= (G2 .order()) + (card (V \ (the_Vertices_of G2))) by GLIB_000:def 24 ; :: thesis: verum