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 )

A2: W .last() = v by A1;

W .first() = v by A1;

hence W is closed by A2; :: thesis: verum

( 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 )

given v being set such that A1:
W is_Walk_from v,v
; :: thesis: 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;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

A2: W .last() = v by A1;

W .first() = v by A1;

hence W is closed by A2; :: thesis: verum