theorem Th18: :: JGRAPH_1:18

for X being non empty set
for f being FinSequence of X st PairF f is Simple & f . 1 <> f . (len f) holds
( f is one-to-one & len f <> 1 )