theorem Th19: :: FINSEQ_6:145

for p being FinSequence holds
( p is TwoValued iff ( len p > 1 & ex x, y being object st
( x <> y & rng p = {x,y} ) ) )