theorem Th138: :: GLIB_010:138

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