theorem :: GLIBPRE1:29

for G being _Graph
for W being Walk of G
for e being object st e in W .edges() & not e in G .loops() & W is Circuit-like holds
ex e0 being object st
( e0 in W .edges() & e0 <> e )