theorem Th1: :: JGRAPH_1:1

for G being Graph
for IT being oriented Chain of G
for vs being FinSequence of the carrier of G st IT is Simple & vs is_oriented_vertex_seq_of IT holds
for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs )