theorem Th63: :: GLIB_007:63

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V
for W being Walk of G1 st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
( ( W .edges() c= the_Edges_of G2 & W is trivial implies not v in W .vertices() ) & ( not v in W .vertices() implies W .edges() c= the_Edges_of G2 ) )