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 :: thesis: for x being object holds
( ( x in (G .walkOf v) .vertices() implies x in {v} ) & ( x in {v} implies x in (G .walkOf v) .vertices() ) )
let x be object ; :: thesis: ( ( x in (G .walkOf v) .vertices() implies x in {v} ) & ( x in {v} implies x in (G .walkOf v) .vertices() ) )
A1: 1 <= len (G .walkOf v) by ABIAN:12;
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
A2: n <= len (G .walkOf v) and
A3: (G .walkOf v) . n = x by Lm45;
A4: 1 <= n by ABIAN:12;
n <= 1 by A2, Th12;
then x = (G .walkOf v) . 1 by A3, A4, XXREAL_0:1;
then x = v by Th12;
hence x in {v} by TARSKI:def 1; :: thesis: verum
end;
assume x in {v} ; :: thesis: x in (G .walkOf v) .vertices()
then A5: x = v by TARSKI:def 1;
(G .walkOf v) . 1 = v by Th12;
hence x in (G .walkOf v) .vertices() by A5, A1, Lm45, JORDAN12:2; :: thesis: verum
end;
hence (G .walkOf v) .vertices() = {v} by TARSKI:2; :: thesis: verum