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() = {} )

then W .edgeSeq() = {} ;

then W .length() = 0 ;

hence W is trivial ; :: thesis: verum

( 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 .edges() = {}
; :: thesis: W is trivial assume
W is trivial
; :: thesis: W .edges() = {}

then W .length() = 0 ;

then W .edgeSeq() = {} ;

hence W .edges() = {} ; :: thesis: verum

end;then W .length() = 0 ;

then W .edgeSeq() = {} ;

hence W .edges() = {} ; :: thesis: verum

then W .edgeSeq() = {} ;

then W .length() = 0 ;

hence W is trivial ; :: thesis: verum