let S be Language; :: thesis: S is infinite
set SS = AllSymbolsOf S;
set L = LettersOf S;
reconsider S0 = S as 1-sorted ;
(LettersOf S) \/ (AllSymbolsOf S) = AllSymbolsOf S by XBOOLE_1:12;
hence S is infinite ; :: thesis: verum