let G be Graph; :: thesis: for sc being oriented simple Chain of G holds sc is OrientedPath of G
let sc be oriented simple Chain of G; :: thesis: sc is OrientedPath of G
assume sc is not OrientedPath of G ; :: thesis: contradiction
then consider m, n being Element of NAT such that
A1: ( 1 <= m & m < n & n <= len sc & sc . m = sc . n ) by GRAPH_1:def 14;
sc is Simple by Th20;
then consider vs being FinSequence of the carrier of G such that
A2: ( vs is_oriented_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 Def7;
A3: len vs = (len sc) + 1 by A2, Def5;
A4: m <= len sc by A1, XXREAL_0:2;
A5: 1 <= n by A1, XXREAL_0:2;
A6: ( 1 <= m & m < n & n <= len vs ) by A1, A3, NAT_1:12;
A7: ( 1 <= m + 1 & m + 1 < n + 1 & n + 1 <= len vs ) by A1, A3, NAT_1:12, XREAL_1:8;
then A8: ( 1 <= m & m < n + 1 & n + 1 <= len vs ) by A1, NAT_1:12;
set v1 = vs /. m;
set v2 = vs /. (m + 1);
A9: sc . m orientedly_joins vs /. m,vs /. (m + 1) by A1, A2, A4, Def5;
set v1' = vs /. n;
set v2' = vs /. (n + 1);
sc . n orientedly_joins vs /. n,vs /. (n + 1) by A1, A2, A5, Def5;
then A10: ( vs /. m = vs /. n & vs /. (m + 1) = vs /. (n + 1) ) by A1, A9, Th2;
( m <= len vs & m + 1 <= len vs & 1 <= n + 1 ) by A7, A8, XXREAL_0:2;
then A11: ( vs /. m = vs . m & vs /. (m + 1) = vs . (m + 1) & vs /. n = vs . n & vs /. (n + 1) = vs . (n + 1) ) by A5, A6, A7, FINSEQ_4:24;
then ( m = 1 & n = len vs ) by A2, A6, A10;
hence contradiction by A2, A7, A10, A11; :: thesis: verum