let G be _Graph; :: thesis: for W being Walk of G st len W <= 3 holds

W is Path-like

let W be Walk of G; :: thesis: ( len W <= 3 implies W is Path-like )

assume A1: len W <= 3 ; :: thesis: W is Path-like

W is Path-like

let W be Walk of G; :: thesis: ( len W <= 3 implies W is Path-like )

assume A1: len W <= 3 ; :: thesis: W is Path-like

now :: thesis: W is Path-like end;

hence
W is Path-like
; :: thesis: verumper cases
( len W = 1 or len W <> 1 )
;

end;

suppose
len W = 1
; :: thesis: W is Path-like

then
W is trivial
by Lm55;

then ex v being Vertex of G st W = G .walkOf v by Lm56;

hence W is Path-like by Lm4; :: thesis: verum

end;then ex v being Vertex of G st W = G .walkOf v by Lm56;

hence W is Path-like by Lm4; :: thesis: verum

suppose A2:
len W <> 1
; :: thesis: W is Path-like

1 <= len W
by ABIAN:12;

then 1 < len W by A2, XXREAL_0:1;

then 1 + 2 <= len W by Th1, JORDAN12:2;

then A3: len W = 3 by A1, XXREAL_0:1;

hence W is Path-like by A4; :: thesis: verum

end;then 1 < len W by A2, XXREAL_0:1;

then 1 + 2 <= len W by Th1, JORDAN12:2;

then A3: len W = 3 by A1, XXREAL_0:1;

A4: now :: thesis: for m, n being odd Element of NAT st m < n & n <= len W & W . m = W . n holds

( m = 1 & n = len W )

W is Trail-like
by A1, Lm61;( m = 1 & n = len W )

let m, n be odd Element of NAT ; :: thesis: ( m < n & n <= len W & W . m = W . n implies ( m = 1 & n = len W ) )

assume that

A5: m < n and

A6: n <= len W and

W . m = W . n ; :: thesis: ( m = 1 & n = len W )

A7: 1 <= m by ABIAN:12;

m < (2 * 1) + 1 by A3, A5, A6, XXREAL_0:2;

then (m + 2) - 2 <= 3 - 2 by Th1;

hence m = 1 by A7, XXREAL_0:1; :: thesis: n = len W

(2 * 0) + 1 < n by A5, A7, XXREAL_0:2;

then 1 + 2 <= n by Th1;

hence n = len W by A3, A6, XXREAL_0:1; :: thesis: verum

end;assume that

A5: m < n and

A6: n <= len W and

W . m = W . n ; :: thesis: ( m = 1 & n = len W )

A7: 1 <= m by ABIAN:12;

m < (2 * 1) + 1 by A3, A5, A6, XXREAL_0:2;

then (m + 2) - 2 <= 3 - 2 by Th1;

hence m = 1 by A7, XXREAL_0:1; :: thesis: n = len W

(2 * 0) + 1 < n by A5, A7, XXREAL_0:2;

then 1 + 2 <= n by Th1;

hence n = len W by A3, A6, XXREAL_0:1; :: thesis: verum

hence W is Path-like by A4; :: thesis: verum