let G be _Graph; :: thesis: for x, e, y being set st e Joins x,y,G holds
G .walkOf x,e,y is Path-like
let x, e, y be set ; :: 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

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 HEYTING3:1;
then 1 < n by A4, XXREAL_0:2;
then 1 + 1 < n + 1 by XREAL_1:10;
then 2 * 1 <= n by NAT_1:13;
then 2 * 1 < n by XXREAL_0:1;
then 2 + 1 < n + 1 by XREAL_1:10;
then A7: 3 <= n by NAT_1:13;
then A8: n = 3 by A2, A5, XXREAL_0:1;

now

assume m <> 1 ; :: thesis: contradiction
then 1 < m by A6, XXREAL_0:1;
then 1 + 1 < m + 1 by XREAL_1:10;
then 2 * 1 <= m by NAT_1:13;
then 2 * 1 < m by XXREAL_0:1;
then 2 + 1 < m + 1 by XREAL_1:10;
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

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:3, 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, Def28; :: thesis: verum