not the_Edges_of G in the_Edges_of G ;
hence for b₁ being addEdge of G,v, the_Edges_of G,w holds not b₁ is edgeless by Th54; :: thesis: verum