set SS = the non degenerated infinite ZeroOneStr ;
B10: 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 B10;
hence not S is degenerated by STRUCT_0:def 8; :: thesis: S is eligible
set g = the adicity of S;
thus not LettersOf S is finite ; :: according to FOMODEL1:def 23 :: thesis: the adicity of S . (TheEqSymbOf S) = - 2
thus the adicity of S . (TheEqSymbOf S) = - 2 by Lm6; :: thesis: verum