theorem :: GLIB_001:127

for G being _Graph
for W being Walk of G st W .first() <> W .last() holds
not W is trivial by Lm55;