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