theorem Th137: :: GLIB_010:137

for G1, G2 being _Graph
for F being non empty PGraphMapping of G1,G2
for W1 being b₃ -defined Walk of G1 holds
( ( W1 is trivial implies F .: W1 is trivial ) & ( W1 is closed implies F .: W1 is closed ) & ( F .: W1 is Trail-like implies W1 is Trail-like ) & ( F .: W1 is Path-like implies W1 is Path-like ) )