consider e being Element of the carrier' of G;
reconsider c = <*e*> as directed Chain of G by Th5;
take c ; :: thesis: ( c is directed & not c is empty & c is one-to-one )
thus c is directed ; :: thesis: ( not c is empty & c is one-to-one )
thus not c is empty ; :: thesis: c is one-to-one
let n, m be Element of NAT ; :: according to GRAPH_1:def 14 :: thesis: ( not 1 <= n or m <= n or not m <= len c or not c . n = c . m )
assume A1: ( 1 <= n & n < m & m <= len c ) ; :: thesis: not c . n = c . m
then 1 < m by XXREAL_0:2;
hence not c . n = c . m by A1, FINSEQ_1:56; :: thesis: verum