let G be _Graph; :: thesis: for W1, W2 being Walk of G st W1 .last() = W2 .first() holds
( len W1 <= len (W1 .append W2) & len W2 <= len (W1 .append W2) )
let W1, W2 be Walk of G; :: thesis: ( W1 .last() = W2 .first() implies ( len W1 <= len (W1 .append W2) & len W2 <= len (W1 .append W2) ) )
set W = W1 .append W2;
assume W1 .last() = W2 .first() ; :: thesis: ( len W1 <= len (W1 .append W2) & len W2 <= len (W1 .append W2) )
then A1: (len (W1 .append W2)) + 1 = (len W1) + (len W2) by Lm9;
1 <= len W2 by ABIAN:12;
then ((len W1) + (len W2)) - (len W2) <= ((len (W1 .append W2)) + 1) - 1 by A1, XREAL_1:13;
hence len W1 <= len (W1 .append W2) ; :: thesis: len W2 <= len (W1 .append W2)
1 <= len W1 by ABIAN:12;
then ((len W2) + (len W1)) - (len W1) <= ((len (W1 .append W2)) + 1) - 1 by A1, XREAL_1:13;
hence len W2 <= len (W1 .append W2) ; :: thesis: verum