:: deftheorem Def8 defines VertexSeparator CHORD:def 8 :
for G being _Graph
for a, b being Vertex of G st a <> b & not a,b are_adjacent holds
for b₄ being Subset of (the_Vertices_of G) holds
( b₄ is VertexSeparator of a,b iff ( not a in b₄ & not b in b₄ & ( for G2 being removeVertices of G,b₄
for W being Walk of G2 holds not W is_Walk_from a,b ) ) );