for X, Y being set
for n being Nat st X <> Y & n > 1 holds
ex a1 being TwoValued Alternating FinSequence st
( rng a1 = {X,Y} & len a1 = n & a1 . 1 = X )