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

per cases ( ( v1 in the_Vertices_of G & not v2 in the_Vertices_of G & not e in the_Edges_of G ) or ( not v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G ) or ( 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 ) ) ) ;

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

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: verum

end;

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

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: verum

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: G1 is _finite

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

end;

end;