theorem Th165: :: GLIB_001:167

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