let G2 be _finite _Graph; :: thesis: for v being object
for G1 being addVertex of G2,v st not v in the_Vertices_of G2 holds
G1 .order() = (G2 .order()) + 1
let v be object ; :: thesis: for G1 being addVertex of G2,v st not v in the_Vertices_of G2 holds
G1 .order() = (G2 .order()) + 1
let G1 be addVertex of G2,v; :: thesis: ( not v in the_Vertices_of G2 implies G1 .order() = (G2 .order()) + 1 )
assume not v in the_Vertices_of G2 ; :: thesis: G1 .order() = (G2 .order()) + 1
then card ({v} \ (the_Vertices_of G2)) = 1 by ZFMISC_1:59, CARD_2:42;
hence G1 .order() = (G2 .order()) + 1 by Th100; :: thesis: verum