theorem Th37: :: GLIB_012:37

for G2 being _Graph
for V being set
for G1 being addLoops of G2,V
for P being Path of G1 holds
( P is Path of G2 or ex v, e being object st
( e Joins v,v,G1 & P = G1 .walkOf (v,e,v) ) )