let G be _Graph; :: thesis: for a, b being Vertex of G st a <> b & not a,b are_adjacent holds
for S being Subset of () holds
( S is VertexSeparator of a,b iff ( not a in S & not b in S & ( for W being Walk of G st W is_Walk_from a,b holds
ex x being Vertex of G st
( x in S & x in W .vertices() ) ) ) )

let a, b be Vertex of G; :: thesis: ( a <> b & not a,b are_adjacent implies for S being Subset of () holds
( S is VertexSeparator of a,b iff ( not a in S & not b in S & ( for W being Walk of G st W is_Walk_from a,b holds
ex x being Vertex of G st
( x in S & x in W .vertices() ) ) ) ) )

assume that
A1: a <> b and
A2: not a,b are_adjacent ; :: thesis: for S being Subset of () holds
( S is VertexSeparator of a,b iff ( not a in S & not b in S & ( for W being Walk of G st W is_Walk_from a,b holds
ex x being Vertex of G st
( x in S & x in W .vertices() ) ) ) )

let S be Subset of (); :: thesis: ( S is VertexSeparator of a,b iff ( not a in S & not b in S & ( for W being Walk of G st W is_Walk_from a,b holds
ex x being Vertex of G st
( x in S & x in W .vertices() ) ) ) )

hereby :: thesis: ( not a in S & not b in S & ( for W being Walk of G st W is_Walk_from a,b holds
ex x being Vertex of G st
( x in S & x in W .vertices() ) ) implies S is VertexSeparator of a,b )
assume A3: S is VertexSeparator of a,b ; :: thesis: ( not a in S & not b in S & ( for W being Walk of G st W is_Walk_from a,b holds
ex x being Vertex of G st
( x in S & x in W .vertices() ) ) )

hence ( not a in S & not b in S ) by A1, A2, Def8; :: thesis: for W being Walk of G st W is_Walk_from a,b holds
ex x being Vertex of G st
( x in S & x in W .vertices() )

then A4: not (the_Vertices_of G) \ S is empty by XBOOLE_0:def 5;
let W be Walk of G; :: thesis: ( W is_Walk_from a,b implies ex x being Vertex of G st
( x in S & x in W .vertices() ) )

assume A5: W is_Walk_from a,b ; :: thesis: ex x being Vertex of G st
( x in S & x in W .vertices() )

now :: thesis: ( ( for x being Vertex of G holds
( not x in S or not x in W .vertices() ) ) implies for G2 being removeVertices of G,S holds contradiction )
end;
hence ex x being Vertex of G st
( x in S & x in W .vertices() ) ; :: thesis: verum
end;
assume that
A13: not a in S and
A14: not b in S and
A15: for W being Walk of G st W is_Walk_from a,b holds
ex x being Vertex of G st
( x in S & x in W .vertices() ) ; :: thesis: S is VertexSeparator of a,b
now :: thesis: for G2 being removeVertices of G,S
for W being Walk of G2 holds not W is_Walk_from a,b
let G2 be removeVertices of G,S; :: thesis: for W being Walk of G2 holds not W is_Walk_from a,b
given W being Walk of G2 such that A16: W is_Walk_from a,b ; :: thesis: contradiction
reconsider W2 = W as Walk of G by GLIB_001:167;
W .last() = b by A16;
then A17: W2 .last() = b ;
now :: thesis: for x being object holds
( ( x in W2 .vertices() implies x in W .vertices() ) & ( x in W .vertices() implies x in W2 .vertices() ) )
let x be object ; :: thesis: ( ( x in W2 .vertices() implies x in W .vertices() ) & ( x in W .vertices() implies x in W2 .vertices() ) )
hereby :: thesis: ( x in W .vertices() implies x in W2 .vertices() ) end;
assume x in W .vertices() ; :: thesis:
then ex n being odd Element of NAT st
( n <= len W2 & W2 . n = x ) by GLIB_001:87;
hence x in W2 .vertices() by GLIB_001:87; :: thesis: verum
end;
then A18: W2 .vertices() = W .vertices() by TARSKI:2;
not (the_Vertices_of G) \ S is empty by ;
then the_Vertices_of G2 = () \ S by GLIB_000:def 37;
then A19: for x being Vertex of G holds
( not x in S or not x in W2 .vertices() ) by ;
W .first() = a by A16;
then W2 .first() = a ;
then W2 is_Walk_from a,b by A17;
hence contradiction by A15, A19; :: thesis: verum
end;
hence S is VertexSeparator of a,b by A1, A2, A13, A14, Def8; :: thesis: verum