let X be set ; :: thesis: for S being Language
for r being relational Element of S
for D being RuleSet of S st {(R2 S)} /\ D = {(R2 S)} & {(R3b S)} /\ D = {(R3b S)} & D /\ {(R3e S)} = {(R3e 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 {(R2 S)} /\ D = {(R2 S)} & {(R3b S)} /\ D = {(R3b S)} & D /\ {(R3e S)} = {(R3e 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 {(R2 S)} /\ D = {(R2 S)} & {(R3b S)} /\ D = {(R3b S)} & D /\ {(R3e S)} = {(R3e S)} & X is D -expanded holds
X -freeInterpreter r is (X,D) -termEq -respecting
let D be RuleSet of S; :: thesis: ( {(R2 S)} /\ D = {(R2 S)} & {(R3b S)} /\ D = {(R3b S)} & D /\ {(R3e S)} = {(R3e S)} & X is D -expanded implies X -freeInterpreter r is (X,D) -termEq -respecting )
assume B0: ( {(R2 S)} /\ D = {(R2 S)} & {(R3b S)} /\ D = {(R3b S)} & D /\ {(R3e S)} = {(R3e 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 = abs (ar r);

now

let x1, x2 be set ; :: thesis: ( [x1,x2] in (abs (ar r)) -placesOf ((X,D) -termEq) implies [((X -freeInterpreter r) . x1),((X -freeInterpreter r) . x2)] in id BOOLEAN )
assume C0: [x1,x2] in (abs (ar r)) -placesOf ((X,D) -termEq) ; :: thesis: [((X -freeInterpreter r) . x1),((X -freeInterpreter r) . x2)] in id BOOLEAN
then consider T1, T2 being abs (ar r) -element Element of (AllTermsOf S) * such that
C1: ( T1 = x1 & T2 = x2 & PairWiseEq (T1,T2) c= X ) by Lm42, B0;
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 ;
C2: ( (r -compound) . x1 = w11 & (r -compound) . x2 = w22 ) by C1, FOMODEL3:def 2;
( w11 in X iff w22 in X ) by C2, B0, C0, Lm46;
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 Lm47, FOMODEL3:6;
hence [((X -freeInterpreter r) . x1),((X -freeInterpreter r) . x2)] in id BOOLEAN by C1; :: thesis: verum

end;

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