let G1 be addEdge of G,v,e,w; :: thesis:

per cases ;

suppose A1: ( v is Vertex of G & w is Vertex of G & not e in the_Edges_of G ) ; :: thesis:

then reconsider v0 = v, w0 = w as Vertex of G ;
let v1 be Vertex of G1; :: according to GLIB_013:def 5 :: thesis:
reconsider v2 = v1 as Vertex of G by A1, GLIB_006:def 11;

per cases ;

suppose ( v2 <> v & v2 <> w ) ; :: thesis:

then v1 .edgesInOut() = v2 .edgesInOut() by GLIBPRE0:48;
hence v1 .edgesInOut() is finite ; :: thesis:

end;

suppose ( v2 = v & v <> w ) ; :: thesis:

then v1 .edgesInOut() = (v0 .edgesInOut()) \/ {e} by A1, GLIBPRE0:49;
hence v1 .edgesInOut() is finite ; :: thesis:

end;

suppose ( v2 = w & v <> w ) ; :: thesis:

then v1 .edgesInOut() = (w0 .edgesInOut()) \/ {e} by A1, GLIBPRE0:50;
hence v1 .edgesInOut() is finite ; :: thesis:

end;

suppose ( v2 = v & v = w ) ; :: thesis:

then v1 .edgesInOut() = (v0 .edgesInOut()) \/ {e} by A1, GLIBPRE0:51;
hence v1 .edgesInOut() is finite ; :: thesis:

end;

end;

end;

suppose ( not v is Vertex of G or not w is Vertex of G or e in the_Edges_of G ) ; :: thesis:

then G1 == G by GLIB_006:def 11;
hence G1 is locally-finite by Th24; :: thesis:

end;

end;