theorem :: GLIB_001:136

for G being _Graph
for W being Walk of G holds
( W is trivial iff W .edges() = {} )