let S be Language; :: thesis: for s being Element of S st s <> TheNorSymbOf S & s <> TheEqSymbOf S holds
s in OwnSymbolsOf S
let s be Element of S; :: thesis: ( s <> TheNorSymbOf S & s <> TheEqSymbOf S implies s in OwnSymbolsOf S )
set O = OwnSymbolsOf S;
set R = RelSymbolsOf S;
set E = TheEqSymbOf S;
set X = (RelSymbolsOf S) \ (OwnSymbolsOf S);
set N = TheNorSymbOf S;
set SS = AllSymbolsOf S;
assume ( s <> TheNorSymbOf S & s <> TheEqSymbOf S ) ; :: thesis: s in OwnSymbolsOf S
then ( not s in {(TheNorSymbOf S)} & not s in {(TheEqSymbOf S)} ) by TARSKI:def 1;
then not s in {(TheNorSymbOf S)} \/ {(TheEqSymbOf S)} by XBOOLE_0:def 3;
hence s in OwnSymbolsOf S by XBOOLE_0:def 5; :: thesis: verum