let G1 be addAdjVertex of G,v1,e,v2; :: thesis:

per cases ;

suppose ( v1 in the_Vertices_of G & not v2 in the_Vertices_of G & not e in the_Edges_of G ) ; :: thesis:

then ( the_Vertices_of G1 = (the_Vertices_of G) \/ {v2} & the_Edges_of G1 = (the_Edges_of G) \/ {e} ) by Def12;
hence G1 is _finite by GLIB_000:def 17; :: thesis:

end;

suppose ( not v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G ) ; :: thesis:

then ( the_Vertices_of G1 = (the_Vertices_of G) \/ {v1} & the_Edges_of G1 = (the_Edges_of G) \/ {e} ) by Def12;
hence G1 is _finite by GLIB_000:def 17; :: thesis:

end;

suppose ( not ( v1 in the_Vertices_of G & not v2 in the_Vertices_of G & not e in the_Edges_of G ) & not ( not v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G ) ) ; :: thesis:

then G1 == G by Def12;
hence G1 is _finite by GLIB_000:89; :: thesis:

end;

end;