let G1 be addAdjVertex of G, the_Vertices_of G, the_Edges_of G,v; :: 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 Th153; :: thesis: verum