set SS = the non degenerated infinite ZeroOneStr ;
A1: 0. the non degenerated infinite ZeroOneStr <> 1. the non degenerated infinite ZeroOneStr ;
set f = the non degenerated infinite ZeroOneStr TrivialArity ;
take S = Language-like(# the carrier of the non degenerated infinite ZeroOneStr , the ZeroF of the non degenerated infinite ZeroOneStr , the OneF of the non degenerated infinite ZeroOneStr ,( the non degenerated infinite ZeroOneStr TrivialArity) #); :: thesis: ( not S is degenerated & S is eligible )
0. S <> 1. S by A1;
hence not S is degenerated ; :: thesis: S is eligible
set g = the adicity of S;
thus LettersOf S is infinite ; :: according to FOMODEL1:def 23 :: thesis: the adicity of S . (TheEqSymbOf S) = - 2
thus the adicity of S . (TheEqSymbOf S) = - 2 by Lm1; :: thesis: verum