set x = the set ;
len <* the set *> <> 2 by FINSEQ_1:39;
hence ex b₁ being FinSequence st
( b₁ is weakly-one-to-one & not b₁ is empty ) ; :: thesis: verum