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

hereby :: thesis: ( W . 1 = W . (len W) implies W is closed )

assume W is closed ; :: thesis: W . 1 = W . (len W)
then W .first() = W .last() by Def24;
hence W . 1 = W . (len W) ; :: thesis: verum

end;

assume W . 1 = W . (len W) ; :: thesis: W is closed
then W .first() = W .last() ;
hence W is closed by Def24; :: thesis: verum