let X be set ; :: thesis: 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 )
let S2 be Language; :: thesis: ( X /\ (LettersOf S2) is infinite implies ex S1 being Language st
( OwnSymbolsOf S1 = X /\ (OwnSymbolsOf S2) & S2 is S1 -extending ) )
set L2 = LettersOf S2;
set O2 = OwnSymbolsOf S2;
set a2 = the adicity of S2;
set E2 = TheEqSymbOf S2;
set N2 = TheNorSymbOf S2;
set SS2 = AllSymbolsOf S2;
reconsider X1 = (AllSymbolsOf S2) /\ X as Subset of (AllSymbolsOf S2) ;
reconsider N22 = TheNorSymbOf S2, E22 = TheEqSymbOf S2 as Element of AllSymbolsOf S2 ;
{E22,N22} is Subset of (AllSymbolsOf S2) ;
then reconsider X2 = {(TheEqSymbOf S2),(TheNorSymbOf S2)} as non empty Subset of (AllSymbolsOf S2) ;
set SS1 = X1 \/ X2;
assume X /\ (LettersOf S2) is infinite ; :: thesis: ex S1 being Language st
( OwnSymbolsOf S1 = X /\ (OwnSymbolsOf S2) & S2 is S1 -extending )
then reconsider L11 = X /\ (LettersOf S2) as infinite set ;
L11 c= (X /\ (AllSymbolsOf S2)) null {(TheEqSymbOf S2),(TheNorSymbOf S2)} by XBOOLE_1:26;
then reconsider SS11 = X1 \/ X2 as infinite Subset of (AllSymbolsOf S2) ;
reconsider AS11 = SS11 \ {(TheNorSymbOf S2)} as infinite Subset of SS11 ;
( TheEqSymbOf S2 in X2 null X1 & not TheEqSymbOf S2 in {(TheNorSymbOf S2)} ) by TARSKI:def 1, TARSKI:def 2;
then reconsider E1 = TheEqSymbOf S2 as Element of AS11 by XBOOLE_0:def 5;
TheNorSymbOf S2 in X2 null X1 by TARSKI:def 2;
then reconsider N1 = TheNorSymbOf S2 as Element of SS11 ;
reconsider D1 = SS11 \ {N1} as infinite Subset of ((AllSymbolsOf S2) \ {(TheNorSymbOf S2)}) by XBOOLE_1:33;
( rng ( the adicity of S2 | D1) c= INT & dom ( the adicity of S2 | D1) = D1 ) by PARTFUN1:def 2;
then reconsider a1 = the adicity of S2 | D1 as Function of (SS11 \ {N1}),INT by FUNCT_2:2;
reconsider a11 = the adicity of S2 | D1 as Subset of the adicity of S2 ;
set S1 = Language-like(# SS11,E1,N1,a1 #);
set O1 = OwnSymbolsOf Language-like(# SS11,E1,N1,a1 #);
set L1 = LettersOf Language-like(# SS11,E1,N1,a1 #);
reconsider IT = Language-like(# SS11,E1,N1,a1 #) as non degenerated Language-like by Def44;
A1: LettersOf Language-like(# SS11,E1,N1,a1 #) = ( the adicity of S2 " {0}) /\ D1 by FUNCT_1:70
.= ((LettersOf S2) /\ SS11) \ {N1} by XBOOLE_1:49
.= (((LettersOf S2) /\ ((AllSymbolsOf S2) /\ X)) \/ ((LettersOf S2) /\ {(TheEqSymbOf S2),(TheNorSymbOf S2)})) \ {(TheNorSymbOf S2)} by XBOOLE_1:23
.= ((((LettersOf S2) null (AllSymbolsOf S2)) /\ X) \/ ((LettersOf S2) /\ {(TheEqSymbOf S2),(TheNorSymbOf S2)})) \ {(TheNorSymbOf S2)} by XBOOLE_1:16
.= (L11 \/ ((LettersOf S2) /\ {(TheEqSymbOf S2),(TheNorSymbOf S2)})) \ {(TheNorSymbOf S2)} ;
(a1 . E1) \+\ ( the adicity of S2 . E1) = {} ;
then ( a1 . E1 = the adicity of S2 . (TheEqSymbOf S2) & the adicity of S2 . (TheEqSymbOf S2) = - 2 ) by Def23, FOMODEL0:29;
then ( the adicity of IT . (TheEqSymbOf IT) = - 2 & LettersOf IT is infinite ) by A1;
then reconsider IT = IT as Language by Def23;
take IT ; :: thesis: ( OwnSymbolsOf IT = X /\ (OwnSymbolsOf S2) & S2 is IT -extending )
(X1 \/ X2) \ X2 = (X1 \ X2) \/ (X2 \ X2) by XBOOLE_1:42
.= (OwnSymbolsOf S2) /\ X by XBOOLE_1:49 ;
hence OwnSymbolsOf IT = X /\ (OwnSymbolsOf S2) ; :: thesis: S2 is IT -extending
thus S2 is IT -extending ; :: thesis: verum