for G being Graph
for m being Nat
for p being cyclic Path of G holds (((m + 1),(len p)) -cut p) ^ ((1,m) -cut p) is cyclic Path of G