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 (2 * (len (W .edgeSeq()))) + 1 = 0 + 1 by Def15;

then W .edgeSeq() = {} ;

then W is Trail-like ;

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

assume A1: W is trivial ; :: thesis: W is Path-like

A2: now :: thesis: for m, n being odd Element of NAT st m < n & n <= len W & W . m = W . n holds

( m = 1 & n = len W )

len W = 1
by A1, Lm55;( m = 1 & n = len W )

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 that

A3: m < n and

A4: n <= len W and

W . m = W . n ; :: thesis: ( m = 1 & n = len W )

A5: 1 <= m by ABIAN:12;

A6: 1 <= n by ABIAN:12;

n <= 1 by A1, A4, Lm55;

hence ( m = 1 & n = len W ) by A3, A5, A6, XXREAL_0:1; :: thesis: verum

end;assume that

A3: m < n and

A4: n <= len W and

W . m = W . n ; :: thesis: ( m = 1 & n = len W )

A5: 1 <= m by ABIAN:12;

A6: 1 <= n by ABIAN:12;

n <= 1 by A1, A4, Lm55;

hence ( m = 1 & n = len W ) by A3, A5, A6, XXREAL_0:1; :: thesis: verum

then (2 * (len (W .edgeSeq()))) + 1 = 0 + 1 by Def15;

then W .edgeSeq() = {} ;

then W is Trail-like ;

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