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