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

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

suppose ( 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 & the_Edges_of G1 = (the_Edges_of G) \/ {e} ) by Def11;
hence G1 is _finite by GLIB_000:def 17; :: thesis: verum

end;

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

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

end;

end;