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