set f = the adicity of S;
set R = RelSymbolsOf S;
s in RelSymbolsOf S by Def17;
then ( s in dom the adicity of S & the adicity of S . s in INT \ NAT ) by FUNCT_1:def 7;
then A1: ( ar s in INT & not ar s in NAT ) by XBOOLE_0:def 5;
reconsider IT = ar s as Element of INT ;
thus ( ar s is negative & ar s is ext-real ) by A1, INT_1:3; :: thesis: verum