let G1 be addAdjVertex of G,v, the_Edges_of G, the_Vertices_of G; :: thesis: not G1 is complete
( not the_Edges_of G in the_Edges_of G & not the_Vertices_of G in the_Vertices_of G ) ;
hence not G1 is complete by Th152; :: thesis: verum