let G be _Graph; :: thesis: for W1, W2 being Walk of G st W1 is Subwalk of W2 holds
len W1 <= len W2
let W1, W2 be Walk of G; :: thesis: ( W1 is Subwalk of W2 implies len W1 <= len W2 )
assume W1 is Subwalk of W2 ; :: thesis: len W1 <= len W2
then ex es being Subset of (W2 .edgeSeq()) st W1 .edgeSeq() = Seq es by Def32;
then 2 * (len (W1 .edgeSeq())) <= 2 * (len (W2 .edgeSeq())) by Th2, XREAL_1:64;
then (2 * (len (W1 .edgeSeq()))) + 1 <= (2 * (len (W2 .edgeSeq()))) + 1 by XREAL_1:7;
then len W1 <= (2 * (len (W2 .edgeSeq()))) + 1 by Def15;
hence len W1 <= len W2 by Def15; :: thesis: verum