let G be Graph; :: thesis: for sc being simple Chain of G holds
( sc is Path of G iff ( len sc = 0 or len sc = 1 or sc . 1 <> sc . 2 ) )
let sc be simple Chain of G; :: thesis: ( sc is Path of G iff ( len sc = 0 or len sc = 1 or sc . 1 <> sc . 2 ) )

hereby :: thesis: ( ( len sc = 0 or len sc = 1 or sc . 1 <> sc . 2 ) implies sc is Path of G )

assume A1: sc is Path of G ; :: thesis: ( not len sc = 0 & not len sc = 1 implies not sc . 1 = sc . 2 )
assume A2: not len sc = 0 ; :: thesis: ( not len sc = 1 implies not sc . 1 = sc . 2 )
assume A3: not len sc = 1 ; :: thesis: not sc . 1 = sc . 2
assume A4: sc . 1 = sc . 2 ; :: thesis: contradiction
len sc > 1 by A2, A3, NAT_1:26;
then 1 + 1 <= len sc by NAT_1:13;
hence contradiction by A1, A4, GRAPH_1:def 14; :: thesis: verum

end;

assume A5: ( len sc = 0 or len sc = 1 or sc . 1 <> sc . 2 ) ; :: thesis: sc is Path of G

per cases ( len sc = 0 or len sc = 1 or sc . 1 <> sc . 2 ) by A5;

suppose len sc = 0 ; :: thesis: sc is Path of G

then for n, m being Element of NAT st 1 <= n & n < m & m <= len sc holds
sc . n <> sc . m ;
hence sc is Path of G by GRAPH_1:def 14; :: thesis: verum

end;

suppose len sc = 1 ; :: thesis: sc is Path of G

then for n, m being Element of NAT st 1 <= n & n < m & m <= len sc holds
sc . n <> sc . m by XXREAL_0:2;
hence sc is Path of G by GRAPH_1:def 14; :: thesis: verum

end;

suppose A6: sc . 1 <> sc . 2 ; :: thesis: sc is Path of G

now

let n, m be Element of NAT ; :: thesis: ( 1 <= n & n < m & m <= len sc implies sc . n <> sc . m )
assume that
A7: 1 <= n and
A8: n < m and
A9: m <= len sc ; :: thesis: sc . n <> sc . m
thus sc . n <> sc . m :: thesis: verum

proof

assume A10: not sc . n <> sc . m ; :: thesis: contradiction
consider vs being FinSequence of the carrier of G such that
A11: ( 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;
A12: len vs = (len sc) + 1 by A11, Def7;
A13: ( n <= len sc & 1 <= m ) by A7, A8, A9, XXREAL_0:2;
then A14: ( n <= len vs & m <= len vs ) by A9, A12, NAT_1:12;
A15: ( 1 <= n + 1 & n + 1 <= len vs & 1 <= m + 1 & m + 1 <= len vs ) by A9, A12, A13, NAT_1:12, XREAL_1:8;
set vn = vs /. n;
set vn1 = vs /. (n + 1);
set vm = vs /. m;
set vm1 = vs /. (m + 1);
A16: ( vs /. n = vs . n & vs /. (n + 1) = vs . (n + 1) & vs /. m = vs . m & vs /. (m + 1) = vs . (m + 1) ) by A7, A13, A14, A15, FINSEQ_4:24;
A17: ( sc . n joins vs /. n,vs /. (n + 1) & sc . m joins vs /. m,vs /. (m + 1) ) by A7, A9, A11, A13, Def7;

per cases ( ( vs /. n = vs /. m & vs /. (n + 1) = vs /. (m + 1) ) or ( vs /. n = vs /. (m + 1) & vs /. (n + 1) = vs /. m ) ) by A10, A17, Th32;

suppose A18: ( vs /. n = vs /. m & vs /. (n + 1) = vs /. (m + 1) ) ; :: thesis: contradiction

n + 1 < m + 1 by A8, XREAL_1:8;
then ( n = 1 & m = len vs & n + 1 = 1 & m + 1 = len vs ) by A7, A8, A11, A14, A15, A16, A18;
hence contradiction ; :: thesis: verum

end;

suppose A19: ( vs /. n = vs /. (m + 1) & vs /. (n + 1) = vs /. m ) ; :: thesis: contradiction

thus contradiction :: thesis: verum

proof

A20: n + 0 < m + 1 by A8, XREAL_1:10;
A21: n + 1 <= m by A8, NAT_1:13;

per cases ( n + 1 = m or n + 1 < m ) by A21, XXREAL_0:1;

suppose A22: n + 1 = m ; :: thesis: contradiction

( n = 1 & m + 1 = len vs ) by A7, A11, A15, A16, A19, A20;
hence contradiction by A6, A10, A22; :: thesis: verum

end;

suppose n + 1 < m ; :: thesis: contradiction

then ( n = 1 & m + 1 = len vs & n + 1 = 1 & m = len vs ) by A7, A11, A14, A15, A16, A19, A20;
hence contradiction ; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

hence sc is Path of G by GRAPH_1:def 14; :: thesis: verum

end;

end;