let G2 be _Graph; :: thesis: for G1 being Supergraph of G2
for W being Walk of G2 holds W is Walk of G1
let G1 be Supergraph of G2; :: thesis: for W being Walk of G2 holds W is Walk of G1
A1: G2 is Subgraph of G1 by Th61;
let W be Walk of G2; :: thesis: W is Walk of G1
thus W is Walk of G1 by A1, GLIB_001:167; :: thesis: verum