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, Def8, CARD_1:27;
A4: len vs = (len c) + 1 by A2, Def7;

A5: now

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;
then k in dom c by A6, FINSEQ_3:25;
hence vs . k <> vs . (k + 1) by A1, A2, Th38; :: thesis: verum

end;

card (G -VSet (rng c)) = 2 by A1, Def8;
then card (rng vs) = 2 by A2, A3, Th34;
hence vs is TwoValued Alternating FinSequence by A5, Def3, Def4; :: thesis: verum