let G be _Graph; :: thesis: for W being Walk of G holds
( W is closed iff ex x being set st W is_Walk_from x,x )
let W be Walk of G; :: thesis: ( W is closed iff ex x being set st W is_Walk_from x,x )

hereby :: thesis: ( ex x being set st W is_Walk_from x,x implies W is closed )

assume W is closed ; :: thesis: ex x being set st W is_Walk_from x,x
then A1: W .first() = W .last() by Def24;
set x = W .first() ;
W is_Walk_from W .first() ,W .first() by A1, Def23;
hence ex x being set st W is_Walk_from x,x ; :: thesis: verum

end;

given v being set such that A2: W is_Walk_from v,v ; :: thesis: W is closed
( W .first() = v & W .last() = v ) by A2, Def23;
hence W is closed by Def24; :: thesis: verum