:: deftheorem Def23 defines eligible FOMODEL1:def 23 :
for S being Language-like holds
( S is eligible iff ( LettersOf S is infinite & the adicity of S . (TheEqSymbOf S) = - 2 ) );