let x be set ; :: thesis: for S being Language holds
( x is string of S iff x is non empty Element of (AllSymbolsOf S) * )
let S be Language; :: thesis: ( x is string of S iff x is non empty Element of (AllSymbolsOf S) * )
set SS = AllSymbolsOf S;
( x is string of S iff ( x in (AllSymbolsOf S) * & not x in {{}} ) ) by XBOOLE_0:def 5;
hence ( x is string of S iff x is non empty Element of (AllSymbolsOf S) * ) ; :: thesis: verum