let G be Graph; for sc being oriented simple Chain of G holds sc is OrientedPath of G
let sc be oriented simple Chain of G; sc is OrientedPath of G
assume
sc is not OrientedPath of G
; contradiction
then consider m, n being Element of NAT such that
A1:
1 <= m
and
A2:
m < n
and
A3:
n <= len sc
and
A4:
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
A5:
vs is_oriented_vertex_seq_of sc
and
A6:
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;
A7:
len vs = (len sc) + 1
by A5, Def5;
A8:
m <= len sc
by A2, A3, XXREAL_0:2;
A9:
1 <= n
by A1, A2, XXREAL_0:2;
A10:
n <= len vs
by A3, A7, NAT_1:12;
A11:
m + 1 < n + 1
by A2, XREAL_1:8;
A12:
n + 1 <= len vs
by A3, A7, XREAL_1:8;
A13:
m < n + 1
by A11, NAT_1:12;
set v1 = vs /. m;
set v2 = vs /. (m + 1);
A14:
sc . m orientedly_joins vs /. m,vs /. (m + 1)
by A1, A5, A8, Def5;
set v19 = vs /. n;
set v29 = vs /. (n + 1);
A15:
sc . n orientedly_joins vs /. n,vs /. (n + 1)
by A3, A5, A9, Def5;
then A16:
vs /. m = vs /. n
by A4, A14, Th2;
A17:
vs /. (m + 1) = vs /. (n + 1)
by A4, A14, A15, Th2;
A18:
m <= len vs
by A12, A13, XXREAL_0:2;
A19:
m + 1 <= len vs
by A11, A12, XXREAL_0:2;
A20:
vs /. m = vs . m
by A1, A18, FINSEQ_4:24;
A21:
vs /. (m + 1) = vs . (m + 1)
by A19, FINSEQ_4:24, NAT_1:12;
A22:
vs /. n = vs . n
by A9, A10, FINSEQ_4:24;
A23:
vs /. (n + 1) = vs . (n + 1)
by A12, FINSEQ_4:24, NAT_1:12;
m = 1
by A1, A2, A6, A10, A16, A20, A22;
hence
contradiction
by A6, A11, A12, A17, A21, A23; verum