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;

( 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()

hence A7:
W1 .edges() c= W2 .edges()
by TARSKI:def 3; :: thesis: W1 .vertices() c= W2 .vertices() 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;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

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

hence
W1 .vertices() c= W2 .vertices()
; :: thesis: verumper cases
( W1 is trivial or not W1 is trivial )
;

end;

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

end;

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

v in W2 .vertices()

hence
W1 .vertices() c= W2 .vertices()
by TARSKI:def 3; :: thesis: verumv 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;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