theorem :: GLIB_001:125

for G being _Graph
for W being Walk of G holds
( W is trivial iff 3 <= len W ) by Lm54;