for G being _Graph
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 H being removeVertices of G,S
for aa being Vertex of H st aa = b holds
for x being Vertex of G st x in S holds
ex y being Vertex of G st
( y in H .reachableFrom aa & x,y are_adjacent )