theorem Th38: :: GLIB_007:38

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexToAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
for e1, u being object holds
( not e1 DJoins u,v,G1 & ( not u in V implies not e1 DJoins v,u,G1 ) & ( for e2 being object st e1 DJoins v,u,G1 & e2 DJoins v,u,G1 holds
e1 = e2 ) )