theorem :: GLIB_010:120

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