theorem :: CHORD:54

for G being _Graph
for C being Path of G st C is Cycle-like & C .length() > 3 holds
for x being Vertex of G st x in C .vertices() holds
ex m, n being odd Nat st
( m + 2 < n & n <= len C & ( not m = 1 or not n = len C ) & ( not m = 1 or not n = (len C) - 2 ) & ( not m = 3 or not n = len C ) & C . m <> C . n & C . m in G .AdjacentSet {x} & C . n in G .AdjacentSet {x} )