let G be finite _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 A1: ( e Joins W .last() ,x,G & not x in W .vertices() ) ; :: thesis: card ((W .addEdge e) .vertices() ) = (card (W .vertices() )) + 1
then card ((W .addEdge e) .vertices() ) = card ((W .vertices() ) \/ {x}) by Th96;
hence card ((W .addEdge e) .vertices() ) = (card (W .vertices() )) + 1 by A1, CARD_2:54; :: thesis: verum