let G be Graph; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ;
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 ;
A13: dom p1 = dom p2 by ;
1 + 1 <= len p1 by ;
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 ;
1 in dom p1 by ;
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 ;
then reconsider p2 = p2 as FinSequence of the carrier of G by ;
take p1 ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: ( 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; :: thesis: ( 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 :: thesis: ( 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 ; :: thesis: for n being Nat st 1 <= n & n <= len c holds
c . n joins p2 /. n,p2 /. (n + 1)

let n be Nat; :: thesis: ( 1 <= n & n <= len c implies c . n joins p2 /. n,p2 /. (n + 1) )
assume that
A17: 1 <= n and
A18: n <= len c ; :: thesis: c . n joins p2 /. n,p2 /. (n + 1)
A19: n <= len p1 by ;
then A20: p2 /. n = p2 . n by ;
A21: n in dom p1 by ;
then p2 . n in {( the Source of G . (c . 1)),( the Target of G . (c . 1))} by ;
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 ;
then A25: p2 /. (n + 1) = p2 . (n + 1) by ;
A26: 1 <= n + 1 by NAT_1:12;
then A27: n + 1 in dom p1 by ;
then p2 . (n + 1) in {( the Source of G . (c . 1)),( the Target of G . (c . 1))} by ;
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 ;
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 ;
p1 . (n + 1) in {( the Source of G . (c . 1)),( the Target of G . (c . 1))} by ;
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 ;
hence c . n joins p2 /. n,p2 /. (n + 1) by A23, A29, A20, A25; :: thesis: verum
end;
hence p2 is_vertex_seq_of c ; :: thesis: 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; :: thesis: ( not p is_vertex_seq_of c or p = p1 or p = p2 )
assume A30: p is_vertex_seq_of c ; :: thesis: ( p = p1 or p = p2 )
then reconsider p9 = p as TwoValued Alternating FinSequence by ;
A31: len p = (len c) + 1 by A30;
rng p = {( the Source of G . (c . 1)),( the Target of G . (c . 1))} by ;
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 ) ; :: thesis: verum