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 )

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

end;

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