set S1 = S;
let S2 be Language-like ; :: thesis: ( S2 is S -extending implies S2 is eligible )
set L1 = LettersOf S;
set L2 = LettersOf S2;
set AS1 = AtomicFormulaSymbolsOf S;
set AS2 = AtomicFormulaSymbolsOf S2;
set a1 = the adicity of S;
set a2 = the adicity of S2;
set E1 = TheEqSymbOf S;
set E2 = TheEqSymbOf S2;
assume A1: S2 is S -extending ; :: thesis: S2 is eligible
then A2: ( dom the adicity of S = AtomicFormulaSymbolsOf S & dom the adicity of S2 = AtomicFormulaSymbolsOf S2 & TheEqSymbOf S = TheEqSymbOf S2 & the adicity of S c= the adicity of S2 ) by FUNCT_2:def 1;
reconsider a11 = the adicity of S as Subset of the adicity of S2 by A1;
a11 " {0} c= the adicity of S2 " {0} by RELAT_1:144;
then reconsider L11 = LettersOf S as Subset of (LettersOf S2) ;
(LettersOf S2) null L11 is infinite ;
hence LettersOf S2 is infinite ; :: according to FOMODEL1:def 23 :: thesis: the adicity of S2 . (TheEqSymbOf S2) = - 2
the adicity of S . (TheEqSymbOf S) = - 2 by Def23;
then TheEqSymbOf S in dom the adicity of S by FUNCT_1:def 2;
then the adicity of S . (TheEqSymbOf S) = ( the adicity of S2 +* a11) . (TheEqSymbOf S) by FUNCT_4:13
.= the adicity of S2 . (TheEqSymbOf S2) by FUNCT_4:98, A2 ;
hence the adicity of S2 . (TheEqSymbOf S2) = - 2 by Def23; :: thesis: verum