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

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

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

end;

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