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

per cases ( ( v in the_Vertices_of G & not e in the_Edges_of G & not w in the_Vertices_of G ) or ( not v in the_Vertices_of G & not e in the_Edges_of G & w in the_Vertices_of G ) or ( ( not v in the_Vertices_of G or e in the_Edges_of G or w in the_Vertices_of G ) & ( v in the_Vertices_of G or e in the_Edges_of G or not w in the_Vertices_of G ) ) ) ;

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

then the_Vertices_of G1 = (the_Vertices_of G) \/ {w} by GLIB_006:def 12;
hence G1 is vertex-finite ; :: thesis: verum

end;

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

then the_Vertices_of G1 = (the_Vertices_of G) \/ {v} by GLIB_006:def 12;
hence G1 is vertex-finite ; :: thesis: verum

end;

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

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

end;

end;