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))
.= the adicity of S " {}
.= {} by RELAT_1:136 ;
then TermSymbolsOf S misses RelSymbolsOf S by XBOOLE_0:def 7;
then B3: (TermSymbolsOf S) \ (RelSymbolsOf S) = TermSymbolsOf S by XBOOLE_1:83;
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 B3, DefTermal0;
then not s in RelSymbolsOf S by XBOOLE_0:def 5;
hence not s is relational by DefRelational; :: thesis: verum