theorem :: FOMODEL1:13

for x being set
for S being Language holds
( x is string of S iff x is non empty FinSequence of AllSymbolsOf S ) by Th12;