let G be Graph; for sc being simple Chain of G st 2 < len sc holds
sc is Path of G
let sc be simple Chain of G; ( 2 < len sc implies sc is Path of G )
assume A1:
2 < len sc
; sc is Path of G
assume
sc is not Path of G
; 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;
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) )
;
contradictionthen
m = 1
by A2, A3, A7, A12, A19, A13;
hence
contradiction
by A7, A17, A15, A20, A16, A21;
verum end; suppose A22:
(
vs /. m = vs /. (n + 1) &
vs /. (m + 1) = vs /. n )
;
contradictionthen A23:
n + 1
= len vs
by A2, A7, A18, A9, A19, A16;
m = 1
by A2, A7, A18, A9, A19, A16, A22;
hence
contradiction
by A1, A7, A8, A12, A20, A13, A22, A23;
verum end;