set W = the V5() Walk of G;
take the V5() Walk of G ; :: thesis: the V5() Walk of G is vertex-distinct
thus the V5() Walk of G is vertex-distinct ; :: thesis: verum