let G1 be addLoops of G,V; :: thesis:

suppose A1: V c= the_Vertices_of G ; :: thesis:

let v1 be Vertex of G1; :: according to GLIB_013:def 5 :: thesis:
reconsider v2 = v1 as Vertex of G by A1, GLIB_012:def 5;

suppose v1 in V ; :: thesis:

then consider e being object such that
( e DJoins v1,v1,G1 & not e in the_Edges_of G ) and
v1 .edgesIn() = (v2 .edgesIn()) \/ {e} and
v1 .edgesOut() = (v2 .edgesOut()) \/ {e} and
A2: v1 .edgesInOut() = (v2 .edgesInOut()) \/ {e} by A1, GLIB_012:42;
thus v1 .edgesInOut() is finite by A2; :: thesis:

end;

suppose not v1 in V ; :: thesis:

then v1 .edgesInOut() = v2 .edgesInOut() by A1, GLIB_012:44;
hence v1 .edgesInOut() is finite ; :: thesis:

end;

end;

end;

suppose not V c= the_Vertices_of G ; :: thesis:

then G1 == G by GLIB_012:def 5;
hence G1 is locally-finite by Th24; :: thesis:

end;

end;