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