:: deftheorem Def7 defines Simple GRAPH_4:def 7 :
for G being Graph
for IT being oriented Chain of G holds
( IT is Simple iff ex vs being FinSequence of the carrier of G st
( vs is_oriented_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 ) ) ) );