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 ;
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 ;
now :: thesis: not m <> 1end;
hence ( m = 1 & n = len (G .walkOf (x,e,y)) ) by ; :: 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 ;
then 1 + 1 <= m by NAT_1:13;
then A12: 2 < n by ;
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 ; :: 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