let G be _Graph; :: thesis: for x, e, y being object st e Joins x,y,G holds
G .walkOf (x,e,y) is Path-like
let x, e, y be object ; :: thesis: ( e Joins x,y,G implies G .walkOf (x,e,y) is Path-like )
set W = G .walkOf (x,e,y);
assume A1: e Joins x,y,G ; :: thesis: G .walkOf (x,e,y) is Path-like
then A2: len (G .walkOf (x,e,y)) = 3 by Lm5;

A3: now :: thesis: for m, n being odd Element of NAT st m < n & n <= len (G .walkOf (x,e,y)) & (G .walkOf (x,e,y)) . m = (G .walkOf (x,e,y)) . n holds
( m = 1 & n = len (G .walkOf (x,e,y)) )

let m, n be odd Element of NAT ; :: thesis: ( m < n & n <= len (G .walkOf (x,e,y)) & (G .walkOf (x,e,y)) . m = (G .walkOf (x,e,y)) . n implies ( m = 1 & n = len (G .walkOf (x,e,y)) ) )
assume that
A4: m < n and
A5: n <= len (G .walkOf (x,e,y)) ; :: thesis: ( (G .walkOf (x,e,y)) . m = (G .walkOf (x,e,y)) . n implies ( m = 1 & n = len (G .walkOf (x,e,y)) ) )
assume (G .walkOf (x,e,y)) . m = (G .walkOf (x,e,y)) . n ; :: thesis: ( m = 1 & n = len (G .walkOf (x,e,y)) )
A6: 1 <= m by ABIAN:12;
then 1 < n by A4, XXREAL_0:2;
then 1 + 1 < n + 1 by XREAL_1:8;
then 2 * 1 <= n by NAT_1:13;
then 2 * 1 < n by XXREAL_0:1;
then 2 + 1 < n + 1 by XREAL_1:8;
then A7: 3 <= n by NAT_1:13;
then A8: n = 3 by A2, A5, XXREAL_0:1;

now :: thesis: not m <> 1

assume m <> 1 ; :: thesis: contradiction
then 1 < m by A6, XXREAL_0:1;
then 1 + 1 < m + 1 by XREAL_1:8;
then 2 * 1 <= m by NAT_1:13;
then 2 * 1 < m by XXREAL_0:1;
then 2 + 1 < m + 1 by XREAL_1:8;
hence contradiction by A4, A8, NAT_1:13; :: thesis: verum

end;

hence ( m = 1 & n = len (G .walkOf (x,e,y)) ) by A2, A5, A7, XXREAL_0:1; :: thesis: verum

end;

now :: thesis: for m, n being even Element of NAT st 1 <= m & m < n & n <= len (G .walkOf (x,e,y)) holds
(G .walkOf (x,e,y)) . m <> (G .walkOf (x,e,y)) . n

let m, n be even Element of NAT ; :: thesis: ( 1 <= m & m < n & n <= len (G .walkOf (x,e,y)) implies (G .walkOf (x,e,y)) . m <> (G .walkOf (x,e,y)) . n )
assume that
A9: 1 <= m and
A10: m < n and
A11: n <= len (G .walkOf (x,e,y)) ; :: thesis: (G .walkOf (x,e,y)) . m <> (G .walkOf (x,e,y)) . n
1 < m by A9, JORDAN12:2, XXREAL_0:1;
then 1 + 1 <= m by NAT_1:13;
then A12: 2 < n by A10, XXREAL_0:2;
n <= 3 by A1, A11, Lm5;
then n < (2 * 1) + 1 by XXREAL_0:1;
hence (G .walkOf (x,e,y)) . m <> (G .walkOf (x,e,y)) . n by A12, NAT_1:13; :: thesis: verum

end;

then G .walkOf (x,e,y) is Trail-like by Lm57;
hence G .walkOf (x,e,y) is Path-like by A3; :: thesis: verum