for G2 being _Graph
for G1 being Supergraph of G2
for W being Walk of G2 holds W is Walk of G1