( not the_Vertices_of G is empty & the_Vertices_of G c= the_Vertices_of G ) ;
then ( not the_Vertices_of G in the_Vertices_of G & the_Vertices_of G is non empty Subset of (the_Vertices_of G) ) ;
hence for b₁ being addAdjVertexAll of G, the_Vertices_of G holds not b₁ is edgeless by Th57; :: thesis: verum