:: deftheorem defines one-to-one GRAPH_1:def 16 :
for G being Graph
for IT being Chain of G holds
( IT is one-to-one iff for n, m being Nat st 1 <= n & n < m & m <= len IT holds
IT . n <> IT . m );