consider W being trivial Walk of G;
take W ; :: thesis: W is vertex-distinct
thus W is vertex-distinct ; :: thesis: verum