let G be _Graph; for W being Walk of G holds W .edges() c= G .edgesBetween (W .vertices())
let W be Walk of G; W .edges() c= G .edgesBetween (W .vertices())
now for e being object st e in W .edges() holds
e in G .edgesBetween (W .vertices())let e be
object ;
( e in W .edges() implies e in G .edgesBetween (W .vertices()) )assume
e in W .edges()
;
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;
verum end;
hence
W .edges() c= G .edgesBetween (W .vertices())
by TARSKI:def 3; verum