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}

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() ) )

hence
(G .walkOf v) .vertices() = {v}
by TARSKI:2; :: thesis: verum( ( 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;

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;A1: 1 <= len (G .walkOf v) by ABIAN:12;

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

assume
x in {v}
; :: thesis: 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;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

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