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

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