for G1, G2 being _Graph
for F being non empty PGraphMapping of G1,G2
for H2 being Subgraph of rng F
for H1 being inducedSubgraph of G1,(F _V) " (the_Vertices_of H2),(F _E) " (the_Edges_of H2)
for W1 being b₃ -defined Walk of G1 st W1 is Walk of H1 holds
F .: W1 is Walk of H2