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 () 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 () & n div 2 <= m & W1 . n = () . m ) by ;
hence e in W2 .edges() by ; :: thesis: verum
end;
hence A7: W1 .edges() c= W2 .edges() by TARSKI:def 3; :: thesis:
now :: thesis: end;
hence W1 .vertices() c= W2 .vertices() ; :: thesis: verum