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

now :: thesis: for e being object st e in W1 .edges() holds
e in W2 .edges()

let e be object ; :: thesis: ( e in W1 .edges() implies e in W2 .edges() )
assume e in W1 .edges() ; :: thesis: e in W2 .edges()
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: verum

end;

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

now :: thesis: W1 .vertices() c= W2 .vertices()

per cases ( not W1 is trivial or not W1 is trivial ) ;

suppose A8: W1 is trivial ; :: thesis: W1 .vertices() c= W2 .vertices()

now :: thesis: for v being object st v in W1 .vertices() holds
v in W2 .vertices()

let v be object ; :: thesis: ( v in W1 .vertices() implies v in W2 .vertices() )
assume v in W1 .vertices() ; :: thesis: v in W2 .vertices()
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: verum

end;

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

end;

suppose W1 is trivial ; :: thesis: W1 .vertices() c= W2 .vertices()

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

end;

end;

end;

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