theorem Th27: :: CHORD:27

for G being _Graph
for P, H being Path of G st P .edges() misses H .edges() & P is open & H is trivial & H is open & (P .vertices()) /\ (H .vertices()) = {(P .first()),(P .last())} & H .first() = P .last() & H .last() = P .first() holds
P .append H is Cycle-like