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