let X be set ; :: thesis: for S being Language
for r being relational Element of S
for D being RuleSet of S st {(R#2 S)} /\ D = {(R#2 S)} & {(R#3b S)} /\ D = {(R#3b S)} & D /\ {(R#3e S)} = {(R#3e S)} & X is D -expanded holds
X -freeInterpreter r is (X,D) -termEq -respecting
let S be Language; :: thesis: for r being relational Element of S
for D being RuleSet of S st {(R#2 S)} /\ D = {(R#2 S)} & {(R#3b S)} /\ D = {(R#3b S)} & D /\ {(R#3e S)} = {(R#3e S)} & X is D -expanded holds
X -freeInterpreter r is (X,D) -termEq -respecting
let r be relational Element of S; :: thesis: for D being RuleSet of S st {(R#2 S)} /\ D = {(R#2 S)} & {(R#3b S)} /\ D = {(R#3b S)} & D /\ {(R#3e S)} = {(R#3e S)} & X is D -expanded holds
X -freeInterpreter r is (X,D) -termEq -respecting
let D be RuleSet of S; :: thesis: ( {(R#2 S)} /\ D = {(R#2 S)} & {(R#3b S)} /\ D = {(R#3b S)} & D /\ {(R#3e S)} = {(R#3e S)} & X is D -expanded implies X -freeInterpreter r is (X,D) -termEq -respecting )
assume A1: ( {(R#2 S)} /\ D = {(R#2 S)} & {(R#3b S)} /\ D = {(R#3b S)} & D /\ {(R#3e S)} = {(R#3e S)} & X is D -expanded ) ; :: thesis: X -freeInterpreter r is (X,D) -termEq -respecting
set AT = AllTermsOf S;
set R = (X,D) -termEq ;
set I = X -freeInterpreter r;
set AF = AtomicFormulasOf S;
set ch = chi (X,(AtomicFormulasOf S));
set SS = AllSymbolsOf S;
set g = r -compound ;
set m = |.(ar r).|;

now :: thesis: for x1, x2 being set st [x1,x2] in |.(ar r).| -placesOf ((X,D) -termEq) holds
[((X -freeInterpreter r) . x1),((X -freeInterpreter r) . x2)] in id BOOLEAN

let x1, x2 be set ; :: thesis: ( [x1,x2] in |.(ar r).| -placesOf ((X,D) -termEq) implies [((X -freeInterpreter r) . x1),((X -freeInterpreter r) . x2)] in id BOOLEAN )
assume A2: [x1,x2] in |.(ar r).| -placesOf ((X,D) -termEq) ; :: thesis: [((X -freeInterpreter r) . x1),((X -freeInterpreter r) . x2)] in id BOOLEAN
then consider T1, T2 being |.(ar r).| -element Element of (AllTermsOf S) * such that
A3: ( T1 = x1 & T2 = x2 & PairWiseEq (T1,T2) c= X ) by Lm37, A1;
reconsider w1 = r -compound T1, w2 = r -compound T2 as 0 -wff string of S ;
( w1 in AtomicFormulasOf S & w2 in AtomicFormulasOf S ) ;
then reconsider w11 = w1, w22 = w2 as Element of AtomicFormulasOf S ;
A4: ( (r -compound) . x1 = w11 & (r -compound) . x2 = w22 ) by A3, FOMODEL3:def 2;
( w11 in X iff w22 in X ) by A4, A1, A2, Lm40;
then ( [((chi (X,(AtomicFormulasOf S))) . w1),((chi (X,(AtomicFormulasOf S))) . w2)] in id BOOLEAN & (X -freeInterpreter r) . T1 = (chi (X,(AtomicFormulasOf S))) . w1 & (X -freeInterpreter r) . T2 = (chi (X,(AtomicFormulasOf S))) . w2 ) by FOMODEL0:67, FOMODEL3:6;
hence [((X -freeInterpreter r) . x1),((X -freeInterpreter r) . x2)] in id BOOLEAN by A3; :: thesis: verum

end;

then X -freeInterpreter r is |.(ar r).| -placesOf ((X,D) -termEq), id BOOLEAN -respecting ;
hence X -freeInterpreter r is (X,D) -termEq -respecting by FOMODEL3:def 10; :: thesis: verum