theorem :: GLIB_001:126

for G being _Graph
for W being Walk of G holds
( W is trivial iff len W <> 1 ) by Lm55;