:: deftheorem Def9 defines simple GRAPH_2:def 5 :
for G being Graph
for IT being Chain of G holds
( IT is simple iff ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of IT & ( for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs ) ) ) );