theorem Th45: :: CHORD:46

for G being _Graph
for W being Walk of G st W .first() <> W .last() & not W .first() ,W .last() are_adjacent holds
W .length() >= 2