for G being _Graph
for W being Walk of G holds
( W is closed iff ex x being set st W is_Walk_from x,x )