theorem Th171: :: GLIB_001:173

for G1 being _Graph
for G2 being Subgraph of G1
for x, y, e being set st e Joins x,y,G2 holds
G1 .walkOf (x,e,y) = G2 .walkOf (x,e,y)