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

per cases ;

suppose ( v in the_Vertices_of G & not e in the_Edges_of G & not w in the_Vertices_of G ) ; :: thesis:

then the_Edges_of G1 = (the_Edges_of G) \/ {e} by GLIB_006:def 12;
hence G1 is edge-finite ; :: thesis:

end;

suppose ( not v in the_Vertices_of G & not e in the_Edges_of G & w in the_Vertices_of G ) ; :: thesis:

then the_Edges_of G1 = (the_Edges_of G) \/ {e} by GLIB_006:def 12;
hence G1 is edge-finite ; :: thesis:

end;

suppose ( ( not v in the_Vertices_of G or e in the_Edges_of G or w in the_Vertices_of G ) & ( v in the_Vertices_of G or e in the_Edges_of G or not w in the_Vertices_of G ) ) ; :: thesis:

then G == G1 by GLIB_006:def 12;
hence G1 is edge-finite by Th8; :: thesis:

end;

end;