theorem :: GLIB_001:103

for G being _Graph
for W being Walk of G
for e being set st e in W .edges() holds
ex v1, v2 being Vertex of G ex n being odd Element of NAT st
( n + 2 <= len W & v1 = W . n & e = W . (n + 1) & v2 = W . (n + 2) & e Joins v1,v2,G ) by Lm47;