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

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