for G being _Graph
for W being Walk of G ex P being Path of G st
( P is_Walk_from W .first() ,W .last() & P is minlength )