let G be Graph; :: thesis:
let c be Chain of G; :: thesis:
assume A1: c alternates_vertices_in G ; :: thesis:
then A2: 1 <= len c by Def8;
consider p1 being FinSequence of the carrier of G such that
A3: p1 is_vertex_seq_of c by Th36;
A4: len p1 = (len c) + 1 by A3, Def7;
then A5: len p1 > 1 by A2, NAT_1:13;
set X = the Source of G . (c . 1);
set Y = the Target of G . (c . 1);
A6: rng p1 = {(the Source of G . (c . 1)),(the Target of G . (c . 1))} by A1, A3, Th39;
A7: p1 is TwoValued Alternating FinSequence by A1, A3, Th40;
A8: ( 1 in dom c & 1 + 1 = 2 ) by A2, FINSEQ_3:27;
then A9: p1 . 1 <> p1 . 2 by A1, A3, Th38;
then consider p2 being TwoValued Alternating FinSequence such that
A10: ( rng p2 = {(p1 . 2),(p1 . 1)} & len p2 = len p1 & p2 . 1 = p1 . 2 ) by A5, Th23;
A11: dom p1 = dom p2 by A10, FINSEQ_3:31;
1 + 1 <= len p1 by A5, NAT_1:13;
then ( 1 <= len p1 & 2 <= len p1 ) by NAT_1:13;
then ( 1 in dom p1 & 2 in dom p1 ) by FINSEQ_3:27;
then ( p1 . 1 in rng p1 & p1 . 2 in rng p1 ) by FUNCT_1:def 5;
then A12: ( ( p1 . 1 = the Source of G . (c . 1) or p1 . 1 = the Target of G . (c . 1) ) & ( p1 . 2 = the Source of G . (c . 1) or p1 . 2 = the Target of G . (c . 1) ) & {(the Source of G . (c . 1)),(the Target of G . (c . 1))} = {(the Target of G . (c . 1)),(the Source of G . (c . 1))} ) by A6, TARSKI:def 2;
then rng p2 c= the carrier of G by A1, A3, A6, A8, A10, Th38, FINSEQ_1:def 4;
then reconsider p2 = p2 as FinSequence of the carrier of G by FINSEQ_1:def 4;
take p1 ; :: thesis:
take p2 ; :: thesis:
thus p1 <> p2 by A1, A3, A8, A10, Th38; :: thesis:
thus p1 is_vertex_seq_of c by A3; :: thesis:

now

thus len p2 = (len c) + 1 by A3, A10, Def7; :: thesis:
let n be Element of NAT ; :: thesis:
assume A13: ( 1 <= n & n <= len c ) ; :: thesis:
set x = p1 /. n;
set y = p1 /. (n + 1);
A14: c . n joins p1 /. n,p1 /. (n + 1) by A3, A13, Def7;
A15: ( 1 <= n & n <= len p1 & 1 <= n + 1 & n + 1 <= len p1 ) by A4, A13, NAT_1:12, XREAL_1:8;
then ( n in dom p1 & n + 1 in dom p1 ) by FINSEQ_3:27;
then ( p1 . n in {(the Source of G . (c . 1)),(the Target of G . (c . 1))} & p1 . (n + 1) in {(the Source of G . (c . 1)),(the Target of G . (c . 1))} & p2 . n in {(the Source of G . (c . 1)),(the Target of G . (c . 1))} & p2 . (n + 1) in {(the Source of G . (c . 1)),(the Target of G . (c . 1))} ) by A1, A3, A6, A8, A10, A11, A12, Th38, FUNCT_1:def 5;
then ( ( p1 . n = the Source of G . (c . 1) or p1 . n = the Target of G . (c . 1) ) & ( p2 . n = the Source of G . (c . 1) or p2 . n = the Target of G . (c . 1) ) & ( p1 . (n + 1) = the Source of G . (c . 1) or p1 . (n + 1) = the Target of G . (c . 1) ) & ( p2 . (n + 1) = the Source of G . (c . 1) or p2 . (n + 1) = the Target of G . (c . 1) ) ) by TARSKI:def 2;
then A16: ( p1 /. (n + 1) = p2 . n & p1 /. n = p2 . (n + 1) ) by A6, A7, A9, A10, A12, A15, Def4, Th21, FINSEQ_4:24;
( p2 /. n = p2 . n & p2 /. (n + 1) = p2 . (n + 1) ) by A10, A15, FINSEQ_4:24;
hence c . n joins p2 /. n,p2 /. (n + 1) by A14, A16, Th31; :: thesis:

end;

hence p2 is_vertex_seq_of c by Def7; :: thesis:
let p be FinSequence of the carrier of G; :: thesis:
assume A17: p is_vertex_seq_of c ; :: thesis:
then reconsider p' = p as TwoValued Alternating FinSequence by A1, Th40;
A18: len p = (len c) + 1 by A17, Def7;
rng p = {(the Source of G . (c . 1)),(the Target of G . (c . 1))} by A1, A17, Th39;
then ( p' = p1 or p' = p2 ) by A4, A6, A7, A9, A10, A12, A18, Th22;
hence ( p = p1 or p = p2 ) ; :: thesis: