let G1 be addAdjVertexAll of G,v,V; :: thesis: G1 is edge-finite

per cases ( ( V c= the_Vertices_of G & not v in the_Vertices_of G ) or not V c= the_Vertices_of G or v in the_Vertices_of G ) ;

suppose ( V c= the_Vertices_of G & not v in the_Vertices_of G ) ; :: thesis: G1 is edge-finite

then consider E being set such that
A1: ( card V = card E & E misses the_Edges_of G ) and
A2: the_Edges_of G1 = (the_Edges_of G) \/ E and
for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) ) by GLIB_007:def 4;
E is finite by A1;
hence G1 is edge-finite by A2; :: thesis: verum

end;

suppose ( not V c= the_Vertices_of G or v in the_Vertices_of G ) ; :: thesis: G1 is edge-finite

then G1 == G by GLIB_007:def 4;
hence G1 is edge-finite by Th8; :: thesis: verum

end;

end;