theorem :: GLIB_010:119

for G1, G2 being _Graph
for F being empty PGraphMapping of G1,G2
for W1 being Walk of G1 holds not W1 is F -defined by XBOOLE_1:3;