let S be non degenerated Language-like ; :: thesis: TheEqSymbOf S in (AllSymbolsOf S) \ {(TheNorSymbOf S)}
set EQ = TheEqSymbOf S;
set NOR = TheNorSymbOf S;
set SS = AllSymbolsOf S;
( 1. S <> 0. S & TheEqSymbOf S = 0. S & TheNorSymbOf S = 1. S ) ;
then ( TheEqSymbOf S in AllSymbolsOf S & not TheEqSymbOf S in {(TheNorSymbOf S)} ) by TARSKI:def 1;
hence TheEqSymbOf S in (AllSymbolsOf S) \ {(TheNorSymbOf S)} by XBOOLE_0:def 5; :: thesis: verum