let X be set ; :: thesis: for S being Language
for D being RuleSet of S
for s being low-compounding Element of S st {(R3d S)} c= D & X is D -expanded & s is termal holds
X -freeInterpreter s is (X,D) -termEq -respecting
let S be Language; :: thesis: for D being RuleSet of S
for s being low-compounding Element of S st {(R3d S)} c= D & X is D -expanded & s is termal holds
X -freeInterpreter s is (X,D) -termEq -respecting
let D be RuleSet of S; :: thesis: for s being low-compounding Element of S st {(R3d S)} c= D & X is D -expanded & s is termal holds
X -freeInterpreter s is (X,D) -termEq -respecting
let s be low-compounding Element of S; :: thesis: ( {(R3d S)} c= D & X is D -expanded & s is termal implies X -freeInterpreter s is (X,D) -termEq -respecting )
set n = abs (ar s);
set AT = AllTermsOf S;
set E = TheEqSymbOf S;
set Phi = X;
set R = (X,D) -termEq ;
set I = X -freeInterpreter s;
assume B1: {(R3d S)} c= D ; :: thesis: ( not X is D -expanded or not s is termal or X -freeInterpreter s is (X,D) -termEq -respecting )
assume B2: X is D -expanded ; :: thesis: ( not s is termal or X -freeInterpreter s is (X,D) -termEq -respecting )
assume s is termal ; :: thesis: X -freeInterpreter s is (X,D) -termEq -respecting
then reconsider ss = s as termal Element of S ;
BB3: not ss is relational ;

now

let x1, x2 be set ; :: thesis: ( [x1,x2] in (abs (ar s)) -placesOf ((X,D) -termEq) implies [((X -freeInterpreter s) . x1),((X -freeInterpreter s) . x2)] in (X,D) -termEq )
assume [x1,x2] in (abs (ar s)) -placesOf ((X,D) -termEq) ; :: thesis: [((X -freeInterpreter s) . x1),((X -freeInterpreter s) . x2)] in (X,D) -termEq
then consider T1, T2 being abs (ar s) -element Element of (AllTermsOf S) * such that
B0: ( T1 = x1 & T2 = x2 & PairWiseEq (T1,T2) c= X ) by Lm42, B2;
set Z = PairWiseEq (T1,T2);
reconsider t1 = ss -compound T1, t2 = ss -compound T2 as termal string of S ;
reconsider ZZ = PairWiseEq (T1,T2) as Subset of X by B0;
{[(PairWiseEq (T1,T2)),((<*(TheEqSymbOf S)*> ^ t1) ^ t2)]} is {} ,{(R3d S)} -derivable by Lm41;
then B4: {[(PairWiseEq (T1,T2)),((<*(TheEqSymbOf S)*> ^ t1) ^ t2)]} is {} ,D -derivable by B1, Lm20;
BB7: (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is ZZ,D -provable by B4, DefProvable;
( (X -freeInterpreter s) . T1 = t1 & (X -freeInterpreter s) . T2 = t2 ) by FOMODEL3:6;
hence [((X -freeInterpreter s) . x1),((X -freeInterpreter s) . x2)] in (X,D) -termEq by BB7, B0; :: thesis: verum

end;

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