theorem Th37: :: CHORD:38

for G being _Graph
for W being Walk of G st ( for P being Path of G st P is_Walk_from W .first() ,W .last() holds
len P >= len W ) holds
W is minlength