let U be non empty set ; :: thesis: for S being Language
for l being literal Element of S
for E being total reflexive Relation of U
for f being Interpreter of l,U holds f is E -respecting
let S be Language; :: thesis: for l being literal Element of S
for E being total reflexive Relation of U
for f being Interpreter of l,U holds f is E -respecting
let l be literal Element of S; :: thesis: for E being total reflexive Relation of U
for f being Interpreter of l,U holds f is E -respecting
let E be total reflexive Relation of U; :: thesis: for f being Interpreter of l,U holds f is E -respecting
reconsider m = |.(ar l).| as zero Nat ;
let f be Interpreter of l,U; :: thesis: f is E -respecting
m -tuples_on U = {{}} by FOMODEL0:10;
then reconsider ff = f as Function of {{}},U by FOMODEL2:def 2;
{} in {{}} by TARSKI:def 1;
then ff is {[{},{}]},E -respecting by Lm50;
then f is m -placesOf E,E -respecting ;
hence f is E -respecting by Def10; :: thesis: verum