for G being chordal _Graph
for P being Path of G st P is open & P is chordless holds
for x, e being object st not x in P .vertices() & e Joins P .last() ,x,G & ( for f being object holds not f Joins P . ((len P) - 2),x,G ) holds
( P .addEdge e is Path-like & P .addEdge e is open & P .addEdge e is chordless )