let G be _Graph; :: thesis: for W being Walk of G holds
( W is V5() iff W .edges() = {} )
let W be Walk of G; :: thesis: ( W is V5() iff W .edges() = {} )

hereby :: thesis: ( W .edges() = {} implies W is V5() )

assume W is V5() ; :: thesis: W .edges() = {}
then W .length() = 0 ;
then W .edgeSeq() = {} ;
hence W .edges() = {} ; :: thesis: verum

end;

assume W .edges() = {} ; :: thesis: W is V5()
then W .edgeSeq() = {} ;
then W .length() = 0 ;
hence W is V5() ; :: thesis: verum