theorem Th12: :: FOMODEL1:12

for x being set
for S being Language holds
( x is string of S iff x is non empty Element of (AllSymbolsOf S) * )