let G2 be _Graph; :: thesis:
let v be object ; :: thesis:
let V be Subset of (the_Vertices_of G2); :: thesis:
let G1 be addAdjVertexAll of G2,v,V; :: thesis:
assume A1: not v in the_Vertices_of G2 ; :: thesis:

hereby :: thesis:

assume A2: ( G2 is locally-finite & V is finite ) ; :: thesis:

now :: thesis:

let v1 be Vertex of G1; :: thesis:

per cases ;

suppose v1 = v ; :: thesis:

then v1 .degree() = card V by A1, GLIBPRE0:57;
hence v1 .degree() is finite by A2; :: thesis:

end;

suppose v1 <> v ; :: thesis:

then A3: not v1 in {v} by TARSKI:def 1;
the_Vertices_of G1 = (the_Vertices_of G2) \/ {v} by A1, GLIB_007:def 4;
then reconsider v2 = v1 as Vertex of G2 by A3, XBOOLE_0:def 3;

per cases ;

suppose not v2 in V ; :: thesis:

then v1 .degree() = v2 .degree() by GLIBPRE0:58;
hence v1 .degree() is finite by A2; :: thesis:

end;

suppose v2 in V ; :: thesis:

then v1 .degree() = (v2 .degree()) +` 1 by A1, GLIBPRE0:59;
hence v1 .degree() is finite by A2; :: thesis:

end;

end;

end;

end;

end;

hence G1 is locally-finite by Th23; :: thesis:

end;

assume A4: G1 is locally-finite ; :: thesis:
G2 is Subgraph of G1 by GLIB_006:57;
hence G2 is locally-finite by A4; :: thesis:
reconsider w = v as Vertex of G1 by A1, GLIB_007:50;
w .degree() is finite by A4;
then card V is finite by A1, GLIBPRE0:57;
hence V is finite ; :: thesis: