let G be _Graph; for W being Walk of G
for e, x being set st e Joins W .last() ,x,G & not x in W .vertices() holds
card ((W .addEdge e) .vertices()) = (card (W .vertices())) + 1
let W be Walk of G; for e, x being set st e Joins W .last() ,x,G & not x in W .vertices() holds
card ((W .addEdge e) .vertices()) = (card (W .vertices())) + 1
let e, x be set ; ( e Joins W .last() ,x,G & not x in W .vertices() implies card ((W .addEdge e) .vertices()) = (card (W .vertices())) + 1 )
assume that
A1:
e Joins W .last() ,x,G
and
A2:
not x in W .vertices()
; card ((W .addEdge e) .vertices()) = (card (W .vertices())) + 1
card ((W .addEdge e) .vertices()) = card ((W .vertices()) \/ {x})
by A1, Th93;
hence
card ((W .addEdge e) .vertices()) = (card (W .vertices())) + 1
by A2, CARD_2:41; verum