consider q being empty oriented Chain of G;
consider x being Element of G;
reconsider p = <*x*> as FinSequence of the carrier of G ;
A1: p is_vertex_seq_of q by Lm1, Th5;
reconsider q9 = q as Chain of G ;
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 )

proof

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
A2: 1 <= n and
A3: n < m and
A4: m <= len p and
p . n = p . m ; :: thesis: ( n = 1 & m = len p )
1 < m by A2, A3, XXREAL_0:2;
hence ( n = 1 & m = len p ) by A4, FINSEQ_1:56; :: thesis: verum

end;

then q9 is simple by A1, GRAPH_2:def 10;
hence ex b₁ being Chain of G st
( b₁ is oriented & b₁ is simple ) ; :: thesis: verum