let W be Walk of G; :: thesis: ( W is trivial implies W is Path-like )
assume A1: W is trivial ; :: thesis: W is Path-like
then len W = 1 by Lm55;
then (2 * (len (W .edgeSeq() ))) + 1 = 0 + 1 by Def15;
then W .edgeSeq() = {} ;
then W .edgeSeq() is one-to-one ;
then A2: W is Trail-like by Def27;

now

let m, n be odd Element of NAT ; :: thesis: ( m < n & n <= len W & W . m = W . n implies ( m = 1 & n = len W ) )
assume A3: ( m < n & n <= len W & W . m = W . n ) ; :: thesis: ( m = 1 & n = len W )
then ( 1 <= m & 1 <= n & n <= 1 ) by A1, Lm55, HEYTING3:1;
hence ( m = 1 & n = len W ) by A3, XXREAL_0:1; :: thesis: verum

end;

hence W is Path-like by A2, Def28; :: thesis: verum