let G be _Graph; :: thesis: for W1, W2 being Walk of G st W1 is_a_prefix_of W2 holds
W1 .edges() c= W2 .edges()
let W1, W2 be Walk of G; :: thesis: ( W1 is_a_prefix_of W2 implies W1 .edges() c= W2 .edges() )
assume A1: W1 c= W2 ; :: thesis: W1 .edges() c= W2 .edges()
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in W1 .edges() or x in W2 .edges() )
assume x in W1 .edges() ; :: thesis: x in W2 .edges()
then consider n being even Element of NAT such that
A2: 1 <= n and
A3: n <= len W1 and
A4: W1 . n = x by GLIB_001:100;
len W1 <= len W2 by A1, FINSEQ_1:84;
then A5: n <= len W2 by A3, XXREAL_0:2;
n in dom W1 by A2, A3, FINSEQ_3:27;
then W2 . n = x by A1, A4, GRFUNC_1:8;
hence x in W2 .edges() by A2, A5, GLIB_001:100; :: thesis: verum