consider x being Element of G;
consider q being empty Chain of G;
reconsider q = q as V7() Chain of G ;
take q ; :: thesis: q is simple
reconsider p = <*x*> as FinSequence of the carrier of G ;
take p ; :: according to GRAPH_2:def 10 :: thesis: ( p is_vertex_seq_of q & ( for n, m being Element of 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 Element of NAT st 1 <= n & n < m & m <= len p & p . n = p . m holds
( n = 1 & m = len p )
let n, m be Element of 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:56; :: thesis: verum