theorem :: FOMODEL1:18

for X being set
for S2 being Language st X /\ (LettersOf S2) is infinite holds
ex S1 being Language st
( OwnSymbolsOf S1 = X /\ (OwnSymbolsOf S2) & S2 is S1 -extending )