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

now

per cases ( len W = 1 or len W <> 1 ) ;

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

then W is trivial by Lm55;
then consider v being Vertex of G such that
A2: W = G .walkOf v by Lm56;
thus W is Path-like by A2, Lm4; :: thesis: verum

end;

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

1 <= len W by HEYTING3:1;
then 1 < len W by A3, XXREAL_0:1;
then 1 + 2 <= len W by Th1, JORDAN12:3;
then A4: len W = 3 by A1, XXREAL_0:1;
A5: W is Trail-like by A1, Lm61;

now

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 A6: ( m < n & n <= len W & W . m = W . n ) ; :: thesis: ( m = 1 & n = len W )
then m < (2 * 1) + 1 by A4, XXREAL_0:2;
then m + 2 <= 3 by Th1;
then A7: (m + 2) - 2 <= 3 - 2 by XREAL_1:15;
A8: 1 <= m by HEYTING3:1;
hence m = 1 by A7, XXREAL_0:1; :: thesis: n = len W
(2 * 0 ) + 1 < n by A6, A8, XXREAL_0:2;
then 1 + 2 <= n by Th1;
hence n = len W by A4, A6, XXREAL_0:1; :: thesis: verum

end;

hence W is Path-like by A5, Def28; :: thesis: verum

end;

end;

end;

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