for G being _Graph
for a, b being Vertex of G st a <> b & not a,b are_adjacent holds
for S being Subset of (the_Vertices_of G) 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() ) ) ) )