let G be Graph; :: thesis: for sc being simple Chain of G st 2 < len sc holds
sc is Path of G
let sc be simple Chain of G; :: thesis: ( 2 < len sc implies sc is Path of G )
assume A1:
2 < len sc
; :: thesis: sc is Path of G
assume
sc is not Path of G
; :: thesis: contradiction
then consider m, n being Element of NAT such that
A2:
( 1 <= m & m < n & n <= len sc & sc . m = sc . n )
by GRAPH_1:def 14;
consider vs being FinSequence of the carrier of G such that
A3:
( vs is_vertex_seq_of sc & ( for n, m being Element of NAT st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs ) ) )
by Def10;
A4:
len vs = (len sc) + 1
by A3, Def7;
A5:
m <= len sc
by A2, XXREAL_0:2;
A6:
1 <= n
by A2, XXREAL_0:2;
A7:
( 1 <= m & m < n & n <= len vs )
by A2, A4, NAT_1:12;
A8:
( 1 <= m + 1 & m + 1 < n + 1 & n + 1 <= len vs )
by A2, A4, NAT_1:12, XREAL_1:8;
then A9:
( 1 <= m & m < n + 1 & n + 1 <= len vs )
by A2, NAT_1:12;
set v1 = vs /. m;
set v2 = vs /. (m + 1);
A10:
sc . m joins vs /. m,vs /. (m + 1)
by A2, A3, A5, Def7;
set v1' = vs /. n;
set v2' = vs /. (n + 1);
A11:
sc . n joins vs /. n,vs /. (n + 1)
by A2, A3, A6, Def7;
( m <= len vs & m + 1 <= len vs & 1 <= n + 1 )
by A8, A9, XXREAL_0:2;
then A12:
( vs /. m = vs . m & vs /. (m + 1) = vs . (m + 1) & vs /. n = vs . n & vs /. (n + 1) = vs . (n + 1) )
by A6, A7, A8, FINSEQ_4:24;