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