let G be _Graph; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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() ; :: thesis: 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; :: thesis: verum