theorem Th31: :: GLIB_009:31

for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() holds
( ( W1 is trivial implies not W2 is trivial ) & ( W1 is closed implies W2 is closed ) )