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 st S is minimal holds
for x being Vertex of G st x in S holds
ex W being Walk of G st
( W is_Walk_from a,b & x in W .vertices() )
let a, b be Vertex of G; :: thesis: ( a <> b & not a,b are_adjacent implies for S being VertexSeparator of a,b st S is minimal holds
for x being Vertex of G st x in S holds
ex W being Walk of G st
( W is_Walk_from a,b & x in W .vertices() ) )
assume that
A1: a <> b and
A2: not a,b are_adjacent ; :: thesis: for S being VertexSeparator of a,b st S is minimal holds
for x being Vertex of G st x in S holds
ex W being Walk of G st
( W is_Walk_from a,b & x in W .vertices() )
let S be VertexSeparator of a,b; :: thesis: ( S is minimal implies for x being Vertex of G st x in S holds
ex W being Walk of G st
( W is_Walk_from a,b & x in W .vertices() ) )
assume A3: S is minimal ; :: thesis: for x being Vertex of G st x in S holds
ex W being Walk of G st
( W is_Walk_from a,b & x in W .vertices() )
let x be Vertex of G; :: thesis: ( x in S implies ex W being Walk of G st
( W is_Walk_from a,b & x in W .vertices() ) )
assume A4: x in S ; :: thesis: ex W being Walk of G st
( W is_Walk_from a,b & x in W .vertices() )
set T = S \ {x};
A5: S \ {x} c= S by XBOOLE_1:36;
then A6: not b in S \ {x} by A1, A2, Def8;
assume A7: for W being Walk of G holds
( not W is_Walk_from a,b or not x in W .vertices() ) ; :: thesis: contradiction

A8: now :: thesis: for W being Walk of G st W is_Walk_from a,b holds
ex y being Vertex of G st
( y in S \ {x} & y in W .vertices() )

let W be Walk of G; :: thesis: ( W is_Walk_from a,b implies ex y being Vertex of G st
( y in S \ {x} & y in W .vertices() ) )
assume A9: W is_Walk_from a,b ; :: thesis: ex y being Vertex of G st
( y in S \ {x} & y in W .vertices() )
consider y being Vertex of G such that
A10: y in S and
A11: y in W .vertices() by A1, A2, A9, Th70;
take y = y; :: thesis: ( y in S \ {x} & y in W .vertices() )
y <> x by A7, A9, A11;
then not y in {x} by TARSKI:def 1;
hence y in S \ {x} by A10, XBOOLE_0:def 5; :: thesis: y in W .vertices()
thus y in W .vertices() by A11; :: thesis: verum

end;

x in {x} by TARSKI:def 1;
then A12: S \ {x} <> S by A4, XBOOLE_0:def 5;
not a in S \ {x} by A1, A2, A5, Def8;
then S \ {x} is VertexSeparator of a,b by A1, A2, A6, A8, Th70;
hence contradiction by A3, A12, A5; :: thesis: verum