let S be Language; :: thesis: (AtomicFormulaSymbolsOf S) \ (OwnSymbolsOf S) = {(TheEqSymbOf S)}
set o = the OneF of S;
set z = the ZeroF of S;
set f = the adicity of S;
set R = RelSymbolsOf S;
set O = OwnSymbolsOf S;
set SS = AllSymbolsOf S;
set e = TheEqSymbOf S;
set n = TheNorSymbOf S;
set A = AtomicFormulaSymbolsOf S;
set D = the carrier of S \ { the OneF of S};
A1: TheEqSymbOf S in AtomicFormulaSymbolsOf S by Lm3;
(AtomicFormulaSymbolsOf S) \ (OwnSymbolsOf S) = (AtomicFormulaSymbolsOf S) \ ((AtomicFormulaSymbolsOf S) \ { the ZeroF of S}) by XBOOLE_1:41
.= ((AtomicFormulaSymbolsOf S) \ (AtomicFormulaSymbolsOf S)) \/ ((AtomicFormulaSymbolsOf S) /\ { the ZeroF of S}) by XBOOLE_1:52
.= { the ZeroF of S} by ZFMISC_1:46, A1 ;
hence (AtomicFormulaSymbolsOf S) \ (OwnSymbolsOf S) = {(TheEqSymbOf S)} ; :: thesis: verum