theorem Th57: :: GLIB_009:57

for G being _Graph
for P being Path of G holds
( P .edges() misses G .loops() or ex v, e being object st
( e Joins v,v,G & P = G .walkOf (v,e,v) ) )