theorem :: GLIB_001:118

for G being _Graph
for W being Walk of G holds
( W is closed iff W . 1 = W . (len W) ) ;