for G being _finite _Graph st ( 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 & not S is empty holds
for G2 being inducedSubgraph of G,S holds G2 is complete ) holds
G is chordal