set W = the trivial Walk of G;

take the trivial Walk of G ; :: thesis: the trivial Walk of G is vertex-distinct

thus the trivial Walk of G is vertex-distinct ; :: thesis: verum

take the trivial Walk of G ; :: thesis: the trivial Walk of G is vertex-distinct

thus the trivial Walk of G is vertex-distinct ; :: thesis: verum