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_{1} being Element of S st b_{1} = TheEqSymbOf S holds

not b_{1} is own
; :: thesis: verum

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

not b