let S be Language; :: thesis: for U being non empty set
for f being Interpreter of S,U holds OwnSymbolsOf S c= dom f
let U be non empty set ; :: thesis: for f being Interpreter of S,U holds OwnSymbolsOf S c= dom f
set SS = AllSymbolsOf S;
set A = AtomicFormulaSymbolsOf S;
set O = OwnSymbolsOf S;
let f be Interpreter of S,U; :: thesis: OwnSymbolsOf S c= dom f

now

let x be set ; :: thesis: ( x in OwnSymbolsOf S implies x in dom f )
assume x in OwnSymbolsOf S ; :: thesis: x in dom f
then reconsider s = x as own Element of S by FOMODEL1:def 19;
not f . s is empty by DefInterpreter2;
hence x in dom f by FUNCT_1:def 2; :: thesis: verum

end;

hence OwnSymbolsOf S c= dom f by TARSKI:def 3; :: thesis: verum