let G1 be addEdge of G,v,e,w; :: thesis: G1 is locally-finite

per cases ( ( v is Vertex of G & w is Vertex of G & not e in the_Edges_of G ) or not v is Vertex of G or not w is Vertex of G or e in the_Edges_of G ) ;

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

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

per cases ( ( v2 <> v & v2 <> w ) or ( v2 = v & v <> w ) or ( v2 = w & v <> w ) or ( v2 = v & v = w ) ) ;

suppose ( v2 <> v & v2 <> w ) ; :: thesis: v1 .edgesInOut() is finite

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

end;

suppose ( v2 = v & v <> w ) ; :: thesis: v1 .edgesInOut() is finite

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

end;

suppose ( v2 = w & v <> w ) ; :: thesis: v1 .edgesInOut() is finite

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

end;

suppose ( v2 = v & v = w ) ; :: thesis: v1 .edgesInOut() is finite

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

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: G1 is locally-finite

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

end;

end;