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

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

hence
W .edges() c= G .edgesBetween (W .vertices())
by TARSKI:def 3; :: thesis: verume 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;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