let G be _Graph; :: thesis: for W being Walk of G holds W .edges() c= G .edgesBetween (W .vertices() )
let W be Walk of G; :: thesis: W .edges() c= G .edgesBetween (W .vertices() )

now

let e be set ; :: thesis: ( e in W .edges() implies e in G .edgesBetween (W .vertices() ) )
assume e in W .edges() ; :: thesis: e in G .edgesBetween (W .vertices() )
then consider v1, v2 being Vertex of G, n being odd Element of NAT such that
A1: ( n + 2 <= len W & v1 = W . n & e = W . (n + 1) & v2 = W . (n + 2) & e Joins v1,v2,G ) by Lm47;
n < len W by A1, Th1;
then A2: v1 in W .vertices() by A1, Lm45;
v2 in W .vertices() by A1, Lm45;
hence e in G .edgesBetween (W .vertices() ) by A1, A2, GLIB_000:35; :: thesis: verum

end;

hence W .edges() c= G .edgesBetween (W .vertices() ) by TARSKI:def 3; :: thesis: verum