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 st (F _V) . (W1 .first()) = (F _V) . (W1 .last()) holds
W1 .first() = W1 .last()