set L = LettersOf S;
card (1 -tuples_on (LettersOf S)) = card (LettersOf S) by CARD_4:8;
hence for b₁ being set st b₁ = AtomicTermsOf S holds
not b₁ is finite ; :: thesis: verum