( not the_Vertices_of G in the_Vertices_of G & not the_Edges_of G in the_Edges_of G ) ;
hence for b₁ being addAdjVertex of G,v, the_Edges_of G, the_Vertices_of G holds not b₁ is edgeless by Th55; :: thesis: verum