let G be _Graph; :: thesis: for W being Walk of G holds
( W is trivial iff ex v being Vertex of G st W = G .walkOf v )
let W be Walk of G; :: thesis: ( W is trivial iff ex v being Vertex of G st W = G .walkOf v )

hereby :: thesis: ( ex v being Vertex of G st W = G .walkOf v implies W is trivial )

assume W is trivial ; :: thesis: ex v being Vertex of G st W = G .walkOf v
then A1: len W = 1 by Lm55;
take v = W .first() ; :: thesis: W = G .walkOf v
thus W = G .walkOf v by A1, FINSEQ_1:57; :: thesis: verum

end;

given v being Vertex of G such that A2: W = G .walkOf v ; :: thesis: W is trivial
len W = 1 by A2, FINSEQ_1:56;
hence W is trivial by Lm55; :: thesis: verum