let S be Language; :: thesis: (AtomicFormulaSymbolsOf S) \ (RelSymbolsOf S) = TermSymbolsOf S
set R = RelSymbolsOf S;
set SSS = AtomicFormulaSymbolsOf S;
set f = the adicity of S;
the adicity of S " INT = AtomicFormulaSymbolsOf S by FUNCT_2:40;
hence (AtomicFormulaSymbolsOf S) \ (RelSymbolsOf S) = the adicity of S " (INT \ (INT \ NAT)) by FUNCT_1:69
.= the adicity of S " ((INT \ INT) \/ (INT /\ NAT)) by XBOOLE_1:52
.= TermSymbolsOf S by XBOOLE_1:7, XBOOLE_1:28 ;
:: thesis: verum