set SS = AllSymbolsOf S;
reconsider C = (AllSymbolsOf S) * as countable set by CARD_4:13;
reconsider IT = C \ {{}} as Subset of C ;
IT is countable ;
hence for b₁ being set st b₁ = ((AllSymbolsOf S) *) \ {{}} holds
b₁ is countable ; :: thesis: verum