let G be _Graph; :: thesis: for a, b being Vertex of G st a <> b & not a,b are_adjacent holds

for S being VertexSeparator of a,b

for W being Walk of G st W is_Walk_from a,b holds

ex k being odd Nat st

( 1 < k & k < len W & W . k in S )

let a, b be Vertex of G; :: thesis: ( a <> b & not a,b are_adjacent implies for S being VertexSeparator of a,b

for W being Walk of G st W is_Walk_from a,b holds

ex k being odd Nat st

( 1 < k & k < len W & W . k in S ) )

assume that

A1: a <> b and

A2: not a,b are_adjacent ; :: thesis: for S being VertexSeparator of a,b

for W being Walk of G st W is_Walk_from a,b holds

ex k being odd Nat st

( 1 < k & k < len W & W . k in S )

let S be VertexSeparator of a,b; :: thesis: for W being Walk of G st W is_Walk_from a,b holds

ex k being odd Nat st

( 1 < k & k < len W & W . k in S )

let W be Walk of G; :: thesis: ( W is_Walk_from a,b implies ex k being odd Nat st

( 1 < k & k < len W & W . k in S ) )

assume A3: W is_Walk_from a,b ; :: thesis: ex k being odd Nat st

( 1 < k & k < len W & W . k in S )

consider x being Vertex of G such that

A4: x in S and

A5: x in W .vertices() by A1, A2, A3, Th70;

consider n being odd Element of NAT such that

A6: n <= len W and

A7: W . n = x by A5, GLIB_001:87;

not a in S by A1, A2, Th70;

then A8: 1 <> n by A3, A4, A7;

not b in S by A1, A2, Th70;

then n <> len W by A3, A4, A7;

then A9: n < len W by A6, XXREAL_0:1;

1 <= n by ABIAN:12;

then 1 < n by A8, XXREAL_0:1;

hence ex k being odd Nat st

( 1 < k & k < len W & W . k in S ) by A4, A7, A9; :: thesis: verum

for S being VertexSeparator of a,b

for W being Walk of G st W is_Walk_from a,b holds

ex k being odd Nat st

( 1 < k & k < len W & W . k in S )

let a, b be Vertex of G; :: thesis: ( a <> b & not a,b are_adjacent implies for S being VertexSeparator of a,b

for W being Walk of G st W is_Walk_from a,b holds

ex k being odd Nat st

( 1 < k & k < len W & W . k in S ) )

assume that

A1: a <> b and

A2: not a,b are_adjacent ; :: thesis: for S being VertexSeparator of a,b

for W being Walk of G st W is_Walk_from a,b holds

ex k being odd Nat st

( 1 < k & k < len W & W . k in S )

let S be VertexSeparator of a,b; :: thesis: for W being Walk of G st W is_Walk_from a,b holds

ex k being odd Nat st

( 1 < k & k < len W & W . k in S )

let W be Walk of G; :: thesis: ( W is_Walk_from a,b implies ex k being odd Nat st

( 1 < k & k < len W & W . k in S ) )

assume A3: W is_Walk_from a,b ; :: thesis: ex k being odd Nat st

( 1 < k & k < len W & W . k in S )

consider x being Vertex of G such that

A4: x in S and

A5: x in W .vertices() by A1, A2, A3, Th70;

consider n being odd Element of NAT such that

A6: n <= len W and

A7: W . n = x by A5, GLIB_001:87;

not a in S by A1, A2, Th70;

then A8: 1 <> n by A3, A4, A7;

not b in S by A1, A2, Th70;

then n <> len W by A3, A4, A7;

then A9: n < len W by A6, XXREAL_0:1;

1 <= n by ABIAN:12;

then 1 < n by A8, XXREAL_0:1;

hence ex k being odd Nat st

( 1 < k & k < len W & W . k in S ) by A4, A7, A9; :: thesis: verum