let G be Graph; for c being Chain of G st c alternates_vertices_in G holds
ex vs1, vs2 being FinSequence of the carrier of G st
( vs1 <> vs2 & vs1 is_vertex_seq_of c & vs2 is_vertex_seq_of c & ( for vs being FinSequence of the carrier of G holds
( not vs is_vertex_seq_of c or vs = vs1 or vs = vs2 ) ) )
let c be Chain of G; ( c alternates_vertices_in G implies ex vs1, vs2 being FinSequence of the carrier of G st
( vs1 <> vs2 & vs1 is_vertex_seq_of c & vs2 is_vertex_seq_of c & ( for vs being FinSequence of the carrier of G holds
( not vs is_vertex_seq_of c or vs = vs1 or vs = vs2 ) ) ) )
set X = the Source of G . (c . 1);
set Y = the Target of G . (c . 1);
consider p1 being FinSequence of the carrier of G such that
A1:
p1 is_vertex_seq_of c
by Th33;
assume A2:
c alternates_vertices_in G
; ex vs1, vs2 being FinSequence of the carrier of G st
( vs1 <> vs2 & vs1 is_vertex_seq_of c & vs2 is_vertex_seq_of c & ( for vs being FinSequence of the carrier of G holds
( not vs is_vertex_seq_of c or vs = vs1 or vs = vs2 ) ) )
then A3:
1 <= len c
;
then A4:
1 in dom c
by FINSEQ_3:25;
A5:
1 + 1 = 2
;
then A6:
p1 . 1 <> p1 . 2
by A2, A1, A4, Th35;
A7:
rng p1 = {( the Source of G . (c . 1)),( the Target of G . (c . 1))}
by A2, A1, Th36;
A8:
len p1 = (len c) + 1
by A1;
then A9:
len p1 > 1
by A3, NAT_1:13;
then consider p2 being TwoValued Alternating FinSequence such that
A10:
rng p2 = {(p1 . 2),(p1 . 1)}
and
A11:
len p2 = len p1
and
A12:
p2 . 1 = p1 . 2
by A6, FINSEQ_6:149;
A13:
dom p1 = dom p2
by A11, FINSEQ_3:29;
1 + 1 <= len p1
by A9, NAT_1:13;
then
2 in dom p1
by FINSEQ_3:25;
then
p1 . 2 in rng p1
by FUNCT_1:def 3;
then A14:
( p1 . 2 = the Source of G . (c . 1) or p1 . 2 = the Target of G . (c . 1) )
by A7, TARSKI:def 2;
1 in dom p1
by A9, FINSEQ_3:25;
then
p1 . 1 in rng p1
by FUNCT_1:def 3;
then A15:
( p1 . 1 = the Source of G . (c . 1) or p1 . 1 = the Target of G . (c . 1) )
by A7, TARSKI:def 2;
then reconsider p2 = p2 as FinSequence of the carrier of G by A2, A1, A7, A4, A5, A10, A14, Th35, FINSEQ_1:def 4;
take
p1
; ex vs2 being FinSequence of the carrier of G st
( p1 <> vs2 & p1 is_vertex_seq_of c & vs2 is_vertex_seq_of c & ( for vs being FinSequence of the carrier of G holds
( not vs is_vertex_seq_of c or vs = p1 or vs = vs2 ) ) )
take
p2
; ( p1 <> p2 & p1 is_vertex_seq_of c & p2 is_vertex_seq_of c & ( for vs being FinSequence of the carrier of G holds
( not vs is_vertex_seq_of c or vs = p1 or vs = p2 ) ) )
thus
p1 <> p2
by A2, A1, A4, A5, A12, Th35; ( p1 is_vertex_seq_of c & p2 is_vertex_seq_of c & ( for vs being FinSequence of the carrier of G holds
( not vs is_vertex_seq_of c or vs = p1 or vs = p2 ) ) )
thus
p1 is_vertex_seq_of c
by A1; ( p2 is_vertex_seq_of c & ( for vs being FinSequence of the carrier of G holds
( not vs is_vertex_seq_of c or vs = p1 or vs = p2 ) ) )
A16:
p1 is TwoValued Alternating FinSequence
by A2, A1, Th37;
now ( len p2 = (len c) + 1 & ( for n being Nat st 1 <= n & n <= len c holds
c . n joins p2 /. n,p2 /. (n + 1) ) )thus
len p2 = (len c) + 1
by A1, A11;
for n being Nat st 1 <= n & n <= len c holds
c . n joins p2 /. n,p2 /. (n + 1)let n be
Nat;
( 1 <= n & n <= len c implies c . n joins p2 /. n,p2 /. (n + 1) )assume that A17:
1
<= n
and A18:
n <= len c
;
c . n joins p2 /. n,p2 /. (n + 1)A19:
n <= len p1
by A8, A18, NAT_1:12;
then A20:
p2 /. n = p2 . n
by A11, A17, FINSEQ_4:15;
A21:
n in dom p1
by A17, A19, FINSEQ_3:25;
then
p2 . n in {( the Source of G . (c . 1)),( the Target of G . (c . 1))}
by A2, A1, A4, A5, A10, A13, A15, A14, Th35, FUNCT_1:def 3;
then A22:
(
p2 . n = the
Source of
G . (c . 1) or
p2 . n = the
Target of
G . (c . 1) )
by TARSKI:def 2;
set x =
p1 /. n;
set y =
p1 /. (n + 1);
A23:
c . n joins p1 /. n,
p1 /. (n + 1)
by A1, A17, A18;
A24:
n + 1
<= len p1
by A8, A18, XREAL_1:6;
then A25:
p2 /. (n + 1) = p2 . (n + 1)
by A11, FINSEQ_4:15, NAT_1:12;
A26:
1
<= n + 1
by NAT_1:12;
then A27:
n + 1
in dom p1
by A24, FINSEQ_3:25;
then
p2 . (n + 1) in {( the Source of G . (c . 1)),( the Target of G . (c . 1))}
by A2, A1, A4, A5, A10, A13, A15, A14, Th35, FUNCT_1:def 3;
then A28:
(
p2 . (n + 1) = the
Source of
G . (c . 1) or
p2 . (n + 1) = the
Target of
G . (c . 1) )
by TARSKI:def 2;
p1 . n in {( the Source of G . (c . 1)),( the Target of G . (c . 1))}
by A7, A21, FUNCT_1:def 3;
then
(
p1 . n = the
Source of
G . (c . 1) or
p1 . n = the
Target of
G . (c . 1) )
by TARSKI:def 2;
then A29:
p1 /. n = p2 . (n + 1)
by A7, A16, A6, A10, A11, A12, A15, A14, A17, A19, A24, A22, A28, FINSEQ_6:def 7, FINSEQ_6:147, FINSEQ_4:15;
p1 . (n + 1) in {( the Source of G . (c . 1)),( the Target of G . (c . 1))}
by A7, A27, FUNCT_1:def 3;
then
(
p1 . (n + 1) = the
Source of
G . (c . 1) or
p1 . (n + 1) = the
Target of
G . (c . 1) )
by TARSKI:def 2;
then
p1 /. (n + 1) = p2 . n
by A7, A16, A6, A10, A11, A12, A15, A14, A17, A26, A24, A22, A28, FINSEQ_6:def 7, FINSEQ_6:147, FINSEQ_4:15;
hence
c . n joins p2 /. n,
p2 /. (n + 1)
by A23, A29, A20, A25;
verum end;
hence
p2 is_vertex_seq_of c
; for vs being FinSequence of the carrier of G holds
( not vs is_vertex_seq_of c or vs = p1 or vs = p2 )
let p be FinSequence of the carrier of G; ( not p is_vertex_seq_of c or p = p1 or p = p2 )
assume A30:
p is_vertex_seq_of c
; ( p = p1 or p = p2 )
then reconsider p9 = p as TwoValued Alternating FinSequence by A2, Th37;
A31:
len p = (len c) + 1
by A30;
rng p = {( the Source of G . (c . 1)),( the Target of G . (c . 1))}
by A2, A30, Th36;
then
( p9 = p1 or p9 = p2 )
by A8, A7, A16, A6, A10, A11, A12, A15, A14, A31, FINSEQ_6:148;
hence
( p = p1 or p = p2 )
; verum