let G be _Graph; :: thesis:
let W1, W2 be Walk of G; :: thesis:
assume A1: W1 is Subwalk of W2 ; :: thesis:
then consider es being Subset of (W2 .edgeSeq()) such that
A2: W1 .edgeSeq() = Seq es by Def32;

now :: thesis:

let e be object ; :: thesis:
assume e in W1 .edges() ; :: thesis:
then consider n being even Element of NAT such that
A3: 1 <= n and
A4: n <= len W1 and
A5: W1 . n = e by Lm46;
A6: W1 . n = (Seq es) . (n div 2) by A2, A3, A4, Lm40;
n div 2 in dom (Seq es) by A2, A3, A4, Lm40;
then ex m being Element of NAT st
( m in dom (W2 .edgeSeq()) & n div 2 <= m & W1 . n = (W2 .edgeSeq()) . m ) by A6, Th3;
hence e in W2 .edges() by A5, Th102; :: thesis:

end;

hence A7: W1 .edges() c= W2 .edges() by TARSKI:def 3; :: thesis:

now :: thesis:

per cases ;

suppose A8: W1 is V5() ; :: thesis:

now :: thesis:

let v be object ; :: thesis:
assume v in W1 .vertices() ; :: thesis:
then consider n being odd Element of NAT such that
A9: n <= len W1 and
A10: W1 . n = v by Lm45;
A11: 1 <= n by ABIAN:12;
n <= 1 by A8, A9, Lm55;
then v = W1 .first() by A10, A11, XXREAL_0:1;
then v = W2 .first() by A1, Th159;
hence v in W2 .vertices() by Th86; :: thesis:

end;

hence W1 .vertices() c= W2 .vertices() by TARSKI:def 3; :: thesis:

end;

suppose W1 is V5() ; :: thesis:

hence W1 .vertices() c= W2 .vertices() by A7, Th132; :: thesis:

end;

end;

end;

hence W1 .vertices() c= W2 .vertices() ; :: thesis: