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 A1: W is trivial ; :: thesis: ex v being Vertex of G st W = G .walkOf v
take v = W .first() ; :: thesis: W = G .walkOf v
len W = 1 by A1, Lm55;
hence W = G .walkOf v by FINSEQ_1:40; :: 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:39;
hence W is trivial by Lm55; :: thesis: verum