let G be _Graph; :: thesis: for W being Walk of G holds

( W is trivial iff W .reverse() is trivial )

let W be Walk of G; :: thesis: ( W is trivial iff W .reverse() is trivial )

thus ( W is trivial implies W .reverse() is trivial ) ; :: thesis: ( W .reverse() is trivial implies W is trivial )

assume W .reverse() is trivial ; :: thesis: W is trivial

then len (W .reverse()) = 1 by Lm55;

then len W = 1 by FINSEQ_5:def 3;

hence W is trivial by Lm55; :: thesis: verum

( W is trivial iff W .reverse() is trivial )

let W be Walk of G; :: thesis: ( W is trivial iff W .reverse() is trivial )

thus ( W is trivial implies W .reverse() is trivial ) ; :: thesis: ( W .reverse() is trivial implies W is trivial )

assume W .reverse() is trivial ; :: thesis: W is trivial

then len (W .reverse()) = 1 by Lm55;

then len W = 1 by FINSEQ_5:def 3;

hence W is trivial by Lm55; :: thesis: verum