for G being Graph
for vs being FinSequence of the carrier of G
for sc being simple Chain of G st vs is_vertex_seq_of sc holds
for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs )