theorem :: GLIBPRE1:130

for G being _Graph
for C being Walk of G
for u, v, w being object st C is Cycle-like & u in C .vertices() & v in C .vertices() & u <> w & v <> w holds
ex W being Path of G st
( W is_Walk_from u,v & not w in W .vertices() )