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 )

len W = 1 by A2, FINSEQ_1:39;

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

( 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 )

given v being Vertex of G such that A2:
W = G .walkOf v
; :: thesis: 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;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

len W = 1 by A2, FINSEQ_1:39;

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