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 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, Th96;
hence card ((W .addEdge e) .vertices() ) = (card (W .vertices() )) + 1 by A2, CARD_2:54; :: thesis: verum