let G be _Graph; :: thesis: for W being Walk of G holds
( W is V5() iff W .reverse() is V5() )
let W be Walk of G; :: thesis: ( W is V5() iff W .reverse() is V5() )
thus ( W is V5() implies W .reverse() is V5() ) ; :: thesis: ( W .reverse() is V5() implies W is V5() )
assume W .reverse() is V5() ; :: thesis: W is V5()
then len (W .reverse()) = 1 by Lm55;
then len W = 1 by FINSEQ_5:def 3;
hence W is V5() by Lm55; :: thesis: verum