set E = TheEqSymbOf S;
set R = RelSymbolsOf S;
set a = the adicity of S;
set D = (AllSymbolsOf S) \ {(TheNorSymbOf S)};
( - 2 in INT & not - 2 in NAT ) by INT_1:def 2;
then B1: - 2 in INT \ NAT by XBOOLE_0:def 5;
( TheEqSymbOf S in (AllSymbolsOf S) \ {(TheNorSymbOf S)} & dom the adicity of S = (AllSymbolsOf S) \ {(TheNorSymbOf S)} ) by Lm5, FUNCT_2:def 1;
then ( TheEqSymbOf S in dom the adicity of S & the adicity of S . (TheEqSymbOf S) in INT \ NAT ) by B1, DefEligible;
then TheEqSymbOf S in RelSymbolsOf S by FUNCT_1:def 7;
hence for b₁ being Element of S st b₁ = TheEqSymbOf S holds
b₁ is relational by DefRelational; :: thesis: verum