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;