let G be Graph; :: thesis: for vs being FinSequence of the carrier of G
for c being Chain of G st c alternates_vertices_in G & vs is_vertex_seq_of c holds
vs is TwoValued Alternating FinSequence
let vs be FinSequence of the carrier of G; :: thesis: for c being Chain of G st c alternates_vertices_in G & vs is_vertex_seq_of c holds
vs is TwoValued Alternating FinSequence
let c be Chain of G; :: thesis: ( c alternates_vertices_in G & vs is_vertex_seq_of c implies vs is TwoValued Alternating FinSequence )
assume that
A1: c alternates_vertices_in G and
A2: vs is_vertex_seq_of c ; :: thesis: vs is TwoValued Alternating FinSequence
A3: c <> {} by A1;
A4: len vs = (len c) + 1 by A2;

A5: now :: thesis: for k being Nat st 1 <= k & k + 1 <= len vs holds
vs . k <> vs . (k + 1)

let k be Nat; :: thesis: ( 1 <= k & k + 1 <= len vs implies vs . k <> vs . (k + 1) )
assume that
A6: 1 <= k and
A7: k + 1 <= len vs ; :: thesis: vs . k <> vs . (k + 1)
k <= len c by A4, A7, XREAL_1:6;
hence vs . k <> vs . (k + 1) by A1, A2, Th35, A6, FINSEQ_3:25; :: thesis: verum

end;

card (rng vs) = 2 by A2, A3, Th31, A1;
hence vs is TwoValued Alternating FinSequence by A5, FINSEQ_6:def 6, FINSEQ_6:def 7; :: thesis: verum