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 V5() implies F .: W1 is V5() ) & ( F .: W1 is V5() implies W1 is V5() ) & ( 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 ) )