let G be _Graph; :: thesis: for v being Vertex of G holds (G .walkOf v) .vertices() = {v}
let v be Vertex of G; :: thesis: (G .walkOf v) .vertices() = {v}

now

let x be set ; :: thesis: ( ( x in (G .walkOf v) .vertices() implies x in {v} ) & ( x in {v} implies x in (G .walkOf v) .vertices() ) )

hereby :: thesis: ( x in {v} implies x in (G .walkOf v) .vertices() )

assume x in (G .walkOf v) .vertices() ; :: thesis: x in {v}
then consider n being odd Element of NAT such that
A1: ( n <= len (G .walkOf v) & (G .walkOf v) . n = x ) by Lm45;
A2: n <= 1 by A1, Th14;
1 <= n by HEYTING3:1;
then x = (G .walkOf v) . 1 by A1, A2, XXREAL_0:1;
then x = v by Th14;
hence x in {v} by TARSKI:def 1; :: thesis: verum

end;

assume x in {v} ; :: thesis: x in (G .walkOf v) .vertices()
then A3: x = v by TARSKI:def 1;
A4: ( 1 <= len (G .walkOf v) & not 1 is even ) by HEYTING3:1, JORDAN12:3;
(G .walkOf v) . 1 = v by Th14;
hence x in (G .walkOf v) .vertices() by A3, A4, Lm45; :: thesis: verum

end;

hence (G .walkOf v) .vertices() = {v} by TARSKI:2; :: thesis: verum