theorem :: CHORD:74

for G being _Graph
for a, b being Vertex of G st a <> b & not a,b are_adjacent & ( for W being Walk of G holds not W is_Walk_from a,b ) holds
{} is VertexSeparator of a,b