set e = the Element of the carrier' of G;
reconsider c = <* the Element of the carrier' of G*> as directed Chain of G by Th4;
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 Nat; :: according to GRAPH_1:def 16 :: thesis: ( not 1 <= n or m <= n or not m <= len c or not c . n = c . m )
assume that
A1: ( 1 <= n & n < m ) and
A2: m <= len c ; :: thesis: not c . n = c . m
1 < m by A1, XXREAL_0:2;
hence not c . n = c . m by A2, FINSEQ_1:39; :: thesis: verum