set T = TermSymbolsOf S;
set R = RelSymbolsOf S;
set f = the adicity of S;
(TermSymbolsOf S) /\ (RelSymbolsOf S) = the adicity of S " (NAT /\ (INT \ NAT)) by FUNCT_1:68
.= the adicity of S " ((NAT /\ INT) \ (NAT /\ NAT))
.= {} ;
then A1: (TermSymbolsOf S) \ (RelSymbolsOf S) = TermSymbolsOf S by XBOOLE_1:83, XBOOLE_0:def 7;
let s be Element of S; :: thesis: ( s is termal implies not s is relational )
assume s is termal ; :: thesis: not s is relational
then s in (TermSymbolsOf S) \ (RelSymbolsOf S) by A1;
then not s in RelSymbolsOf S by XBOOLE_0:def 5;
hence not s is relational ; :: thesis: verum