set E = TheEqSymbOf S;
set R = RelSymbolsOf S;
set O = OwnSymbolsOf S;
TheEqSymbOf S in {(TheEqSymbOf S)} by TARSKI:def 1;
then TheEqSymbOf S in (RelSymbolsOf S) \ (OwnSymbolsOf S) by FOMODEL1:1;
then not TheEqSymbOf S in OwnSymbolsOf S by XBOOLE_0:def 5;
hence for b₁ being Element of S st b₁ = TheEqSymbOf S holds
not b₁ is own ; :: thesis: verum