theorem Th167: :: GLIB_001:169

for G1 being _Graph
for G2 being Subgraph of G1
for W being Walk of G1 st W is trivial & W .edges() c= the_Edges_of G2 holds
W is Walk of G2