let G2 be _Graph; :: thesis: for v being object
for V being Subset of (the_Vertices_of G2)
for G1 being addAdjVertexAll of G2,v,V st not v in the_Vertices_of G2 holds
( ( G2 is locally-finite & V is finite ) iff G1 is locally-finite )
let v be object ; :: thesis: for V being Subset of (the_Vertices_of G2)
for G1 being addAdjVertexAll of G2,v,V st not v in the_Vertices_of G2 holds
( ( G2 is locally-finite & V is finite ) iff G1 is locally-finite )
let V be Subset of (the_Vertices_of G2); :: thesis: for G1 being addAdjVertexAll of G2,v,V st not v in the_Vertices_of G2 holds
( ( G2 is locally-finite & V is finite ) iff G1 is locally-finite )
let G1 be addAdjVertexAll of G2,v,V; :: thesis: ( not v in the_Vertices_of G2 implies ( ( G2 is locally-finite & V is finite ) iff G1 is locally-finite ) )
assume A1: not v in the_Vertices_of G2 ; :: thesis: ( ( G2 is locally-finite & V is finite ) iff G1 is locally-finite )

hereby :: thesis: ( G1 is locally-finite implies ( G2 is locally-finite & V is finite ) )

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

now :: thesis: for v1 being Vertex of G1 holds v1 .degree() is finite

let v1 be Vertex of G1; :: thesis: b₁ .degree() is finite

per cases ( v1 = v or v1 <> v ) ;

suppose v1 = v ; :: thesis: b₁ .degree() is finite

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

end;

suppose v1 <> v ; :: thesis: b₁ .degree() is finite

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 ( not v2 in V or v2 in V ) ;

suppose not v2 in V ; :: thesis: b₁ .degree() is finite

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

end;

suppose v2 in V ; :: thesis: b₁ .degree() is finite

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

end;

end;

end;

end;

end;

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

end;

assume A4: G1 is locally-finite ; :: thesis: ( G2 is locally-finite & V is finite )
G2 is Subgraph of G1 by GLIB_006:57;
hence G2 is locally-finite by A4; :: thesis: V is finite
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:55;
hence V is finite ; :: thesis: verum