let G be _Graph; :: thesis: for W being Walk of G st len W <= 3 holds
W is Trail-like
let W be Walk of G; :: thesis: ( len W <= 3 implies W is Trail-like )
assume A1: len W <= 3 ; :: thesis: W is Trail-like

now :: thesis: W is Trail-like

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

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

then W is trivial by Lm55;
then ex v being Vertex of G st W = G .walkOf v by Lm56;
hence W is Trail-like by Lm4; :: thesis: verum

end;

suppose A2: len W <> 1 ; :: thesis: W is Trail-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;

now :: thesis: for m, n being even Element of NAT st 1 <= m & m < n & n <= len W holds
W . m <> W . n

let m, n be even Element of NAT ; :: thesis: ( 1 <= m & m < n & n <= len W implies W . m <> W . n )
assume that
A4: 1 <= m and
A5: m < n and
A6: n <= len W ; :: thesis: W . m <> W . n
(2 * 0) + 1 < m by A4, XXREAL_0:1;
then A7: 1 + 1 <= m by NAT_1:13;
n < 2 + 1 by A3, A6, XXREAL_0:1;
then n <= 2 by NAT_1:13;
hence W . m <> W . n by A5, A7, XXREAL_0:2; :: thesis: verum

end;

hence W is Trail-like by Lm57; :: thesis: verum

end;

end;

end;

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