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

per cases ( ( v in the_Vertices_of G & not w in the_Vertices_of G & not e in the_Edges_of G ) or ( not v in the_Vertices_of G & w in the_Vertices_of G & not e in the_Edges_of G ) or ( not ( v in the_Vertices_of G & not w in the_Vertices_of G & not e in the_Edges_of G ) & not ( not v in the_Vertices_of G & w in the_Vertices_of G & not e in the_Edges_of G ) ) ) ;

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

then consider G3 being addVertex of G,w such that
A2: G1 is addEdge of G3,v,e,w by GLIB_006:125;
thus G1 is locally-finite by A2; :: thesis: verum

end;

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

then consider G3 being addVertex of G,v such that
A3: G1 is addEdge of G3,v,e,w by GLIB_006:126;
thus G1 is locally-finite by A3; :: thesis: verum

end;

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

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

end;

end;