let G1 be addEdge of G,v,e,w; :: thesis: G1 is vertex-finite

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

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

hence G1 is vertex-finite by GLIB_006:def 11; :: thesis: verum

end;

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

then G == G1 by GLIB_006:def 11;
hence G1 is vertex-finite by Th8; :: thesis: verum

end;

end;