let W be Walk of G; :: thesis: ( W is V5() implies W is Path-like )
assume A1: W is V5() ; :: 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 )
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;
len W = 1 by A1, Lm55;
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