set x = the Element of G;

set q = the empty Chain of G;

reconsider q = the empty Chain of G as V17() Chain of G ;

take q ; :: thesis: q is simple

reconsider p = <* the Element of G*> as FinSequence of the carrier of G ;

take p ; :: according to GRAPH_2:def 5 :: thesis: ( p is_vertex_seq_of q & ( for n, m being Nat st 1 <= n & n < m & m <= len p & p . n = p . m holds

( n = 1 & m = len p ) ) )

thus p is_vertex_seq_of q by Lm8; :: thesis: for n, m being Nat st 1 <= n & n < m & m <= len p & p . n = p . m holds

( n = 1 & m = len p )

let n, m be Nat; :: thesis: ( 1 <= n & n < m & m <= len p & p . n = p . m implies ( n = 1 & m = len p ) )

assume that

A1: 1 <= n and

A2: n < m and

A3: m <= len p and

p . n = p . m ; :: thesis: ( n = 1 & m = len p )

1 < m by A1, A2, XXREAL_0:2;

hence ( n = 1 & m = len p ) by A3, FINSEQ_1:39; :: thesis: verum

set q = the empty Chain of G;

reconsider q = the empty Chain of G as V17() Chain of G ;

take q ; :: thesis: q is simple

reconsider p = <* the Element of G*> as FinSequence of the carrier of G ;

take p ; :: according to GRAPH_2:def 5 :: thesis: ( p is_vertex_seq_of q & ( for n, m being Nat st 1 <= n & n < m & m <= len p & p . n = p . m holds

( n = 1 & m = len p ) ) )

thus p is_vertex_seq_of q by Lm8; :: thesis: for n, m being Nat st 1 <= n & n < m & m <= len p & p . n = p . m holds

( n = 1 & m = len p )

let n, m be Nat; :: thesis: ( 1 <= n & n < m & m <= len p & p . n = p . m implies ( n = 1 & m = len p ) )

assume that

A1: 1 <= n and

A2: n < m and

A3: m <= len p and

p . n = p . m ; :: thesis: ( n = 1 & m = len p )

1 < m by A1, A2, XXREAL_0:2;

hence ( n = 1 & m = len p ) by A3, FINSEQ_1:39; :: thesis: verum