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;

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

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)) )

( 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;

end;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

hence
( m = 1 & n = len (G .walkOf (x,e,y)) )
by A2, A5, A7, XXREAL_0:1; :: thesis: verumassume
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;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

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

then
G .walkOf (x,e,y) is Trail-like
by Lm57;(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;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

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