let G be _Graph; 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 ; ( 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
; G .walkOf (x,e,y) is Path-like
then A2:
len (G .walkOf (x,e,y)) = 3
by Lm5;
A3:
now 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 ;
( 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))
;
( (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
;
( 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;
hence
(
m = 1 &
n = len (G .walkOf (x,e,y)) )
by A2, A5, A7, XXREAL_0:1;
verum end;
now 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)) . nlet m,
n be
even Element of
NAT ;
( 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))
;
(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;
verum end;
then
G .walkOf (x,e,y) is Trail-like
by Lm57;
hence
G .walkOf (x,e,y) is Path-like
by A3; verum