let W be Walk of G; :: thesis: ( W is trivial implies W is vertex-distinct )
assume A4: W is trivial ; :: thesis: W is vertex-distinct

now

let m, n be odd Element of NAT ; :: thesis: ( m <= len W & n <= len W & W . m = W . n implies m = n )
assume ( m <= len W & n <= len W & W . m = W . n ) ; :: thesis: m = n
then ( m <= 1 & n <= 1 & 1 <= m & 1 <= n ) by A4, Lm55, HEYTING3:1;
then ( m = 1 & n = 1 ) by XXREAL_0:1;
hence m = n ; :: thesis: verum

end;

hence W is vertex-distinct by Def29; :: thesis: verum