let G1 be addAdjVertexAll of G, the_Vertices_of G; :: thesis: G1 is complete
( the_Vertices_of G c= the_Vertices_of G & not the_Vertices_of G in the_Vertices_of G ) ;
hence G1 is complete by Th75; :: thesis: verum