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
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in OwnSymbolsOf S or 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 Def3;
hence x in dom f by FUNCT_1:def 2; :: thesis: verum