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 Nat such that

A2: 1 <= m and

A3: m < n and

A4: n <= len sc and

A5: sc . m = sc . n by GRAPH_1:def 16;

consider vs being FinSequence of the carrier of G such that

A6: vs is_vertex_seq_of sc and

A7: for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds

( n = 1 & m = len vs ) by Def9;

A8: len vs = (len sc) + 1 by A6;

then A9: n + 1 <= len vs by A4, XREAL_1:6;

set v29 = vs /. (n + 1);

set v19 = vs /. n;

A10: 1 <= n by A2, A3, XXREAL_0:2;

then A11: sc . n joins vs /. n,vs /. (n + 1) by A4, A6;

A12: n <= len vs by A4, A8, NAT_1:12;

then A13: vs /. n = vs . n by A10, FINSEQ_4:15;

set v1 = vs /. m;

set v2 = vs /. (m + 1);

m <= len sc by A3, A4, XXREAL_0:2;

then A14: sc . m joins vs /. m,vs /. (m + 1) by A2, A6;

A15: n + 1 <= len vs by A4, A8, XREAL_1:6;

then A16: vs /. (n + 1) = vs . (n + 1) by FINSEQ_4:15, NAT_1:12;

A17: m + 1 < n + 1 by A3, XREAL_1:6;

then A18: m < n + 1 by NAT_1:12;

then m <= len vs by A15, XXREAL_0:2;

then A19: vs /. m = vs . m by A2, FINSEQ_4:15;

m + 1 <= len vs by A17, A15, XXREAL_0:2;

then A20: vs /. (m + 1) = vs . (m + 1) by FINSEQ_4:15, NAT_1:12;

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 Nat such that

A2: 1 <= m and

A3: m < n and

A4: n <= len sc and

A5: sc . m = sc . n by GRAPH_1:def 16;

consider vs being FinSequence of the carrier of G such that

A6: vs is_vertex_seq_of sc and

A7: for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds

( n = 1 & m = len vs ) by Def9;

A8: len vs = (len sc) + 1 by A6;

then A9: n + 1 <= len vs by A4, XREAL_1:6;

set v29 = vs /. (n + 1);

set v19 = vs /. n;

A10: 1 <= n by A2, A3, XXREAL_0:2;

then A11: sc . n joins vs /. n,vs /. (n + 1) by A4, A6;

A12: n <= len vs by A4, A8, NAT_1:12;

then A13: vs /. n = vs . n by A10, FINSEQ_4:15;

set v1 = vs /. m;

set v2 = vs /. (m + 1);

m <= len sc by A3, A4, XXREAL_0:2;

then A14: sc . m joins vs /. m,vs /. (m + 1) by A2, A6;

A15: n + 1 <= len vs by A4, A8, XREAL_1:6;

then A16: vs /. (n + 1) = vs . (n + 1) by FINSEQ_4:15, NAT_1:12;

A17: m + 1 < n + 1 by A3, XREAL_1:6;

then A18: m < n + 1 by NAT_1:12;

then m <= len vs by A15, XXREAL_0:2;

then A19: vs /. m = vs . m by A2, FINSEQ_4:15;

m + 1 <= len vs by A17, A15, XXREAL_0:2;

then A20: vs /. (m + 1) = vs . (m + 1) by FINSEQ_4:15, NAT_1:12;

per cases
( ( vs /. m = vs /. n & vs /. (m + 1) = vs /. (n + 1) ) or ( vs /. m = vs /. (n + 1) & vs /. (m + 1) = vs /. n ) )
by A5, A14, A11;

end;