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

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