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 ;
set v29 = vs /. (n + 1);
set v19 = vs /. n;
A10: 1 <= n by ;
then A11: sc . n joins vs /. n,vs /. (n + 1) by A4, A6;
A12: n <= len vs by ;
then A13: vs /. n = vs . n by ;
set v1 = vs /. m;
set v2 = vs /. (m + 1);
m <= len sc by ;
then A14: sc . m joins vs /. m,vs /. (m + 1) by A2, A6;
A15: n + 1 <= len vs by ;
then A16: vs /. (n + 1) = vs . (n + 1) by ;
A17: m + 1 < n + 1 by ;
then A18: m < n + 1 by NAT_1:12;
then m <= len vs by ;
then A19: vs /. m = vs . m by ;
m + 1 <= len vs by ;
then A20: vs /. (m + 1) = vs . (m + 1) by ;
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;
suppose A21: ( vs /. m = vs /. n & vs /. (m + 1) = vs /. (n + 1) ) ; :: thesis: contradiction
end;
suppose A22: ( vs /. m = vs /. (n + 1) & vs /. (m + 1) = vs /. n ) ; :: thesis: contradiction
end;
end;