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 :: thesis: for e being object st e in W .edges() holds
e in G .edgesBetween (W .vertices())

let e be object ; :: 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 and
A2: v1 = W . n and
e = W . (n + 1) and
A3: v2 = W . (n + 2) and
A4: e Joins v1,v2,G by Lm47;
n < len W by A1, Th1;
then A5: v1 in W .vertices() by A2, Lm45;
v2 in W .vertices() by A1, A3, Lm45;
hence e in G .edgesBetween (W .vertices()) by A4, A5, GLIB_000:32; :: thesis: verum

end;

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