let G be _Graph; for W being vertex-distinct Walk of G
for e, v being object st e Joins W .last() ,v,G & not v in W .vertices() holds
W .addEdge e is vertex-distinct
let W be vertex-distinct Walk of G; for e, v being object st e Joins W .last() ,v,G & not v in W .vertices() holds
W .addEdge e is vertex-distinct
let e, v be object ; ( e Joins W .last() ,v,G & not v in W .vertices() implies W .addEdge e is vertex-distinct )
assume that
A1:
e Joins W .last() ,v,G
and
A2:
not v in W .vertices()
; W .addEdge e is vertex-distinct
set W2 = W .addEdge e;
A3:
len (W .addEdge e) = (len W) + 2
by A1, Lm37;
hence
W .addEdge e is vertex-distinct
; verum