let G2 be _finite _Graph; :: thesis: for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
G1 .order() = (G2 .order()) + 1
let v be object ; :: thesis: for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
G1 .order() = (G2 .order()) + 1
let V be set ; :: thesis: for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
G1 .order() = (G2 .order()) + 1
let G1 be addAdjVertexAll of G2,v,V; :: thesis: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 implies G1 .order() = (G2 .order()) + 1 )
assume A1: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) ; :: thesis: G1 .order() = (G2 .order()) + 1
then A2: the_Vertices_of G1 = (the_Vertices_of G2) \/ {v} by Def4;
thus G1 .order() = card (the_Vertices_of G1) by GLIB_000:def 24
.= (card (the_Vertices_of G2)) + 1 by A1, A2, CARD_2:41
.= (G2 .order()) + 1 by GLIB_000:def 24 ; :: thesis: verum