theorem Th57: :: GLIB_007:57

for G2 being _Graph
for v being object
for V being set
for W being Subset of V
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
ex f being Function of W,(G1 .edgesBetween (W,{v})) st
( f is one-to-one & f is onto & ( for w being object st w in W holds
f . w Joins w,v,G1 ) )