let X be set ; :: thesis: for S being Language
for a being ofAtomicFormula Element of S
for D being RuleSet of S st {(R#3a S)} c= D & D /\ {(R#3d S)} = {(R#3d S)} & {(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 a is (X,D) -termEq -respecting
let S be Language; :: thesis: for a being ofAtomicFormula Element of S
for D being RuleSet of S st {(R#3a S)} c= D & D /\ {(R#3d S)} = {(R#3d S)} & {(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 a is (X,D) -termEq -respecting
let a be ofAtomicFormula Element of S; :: thesis: for D being RuleSet of S st {(R#3a S)} c= D & D /\ {(R#3d S)} = {(R#3d S)} & {(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 a is (X,D) -termEq -respecting
let D be RuleSet of S; :: thesis: ( {(R#3a S)} c= D & D /\ {(R#3d S)} = {(R#3d S)} & {(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 a is (X,D) -termEq -respecting )
set s = a;
set AT = AllTermsOf S;
set I = X -freeInterpreter a;
set AF = AtomicFormulasOf S;
set ch = chi (X,(AtomicFormulasOf S));
set SS = AllSymbolsOf S;
set n = |.(ar a).|;
set f = a -compound ;
set R = (X,D) -termEq ;
assume A1: ( {(R#3a S)} c= D & D /\ {(R#3d S)} = {(R#3d S)} & {(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 a is (X,D) -termEq -respecting
then reconsider S2 = {(R#2 S)}, S3 = {(R#3b S)} as Subset of D ;
A2: S2 \/ S3 c= D ;

per cases ( not a is relational or a is relational ) ;

suppose not a is relational ; :: thesis: X -freeInterpreter a is (X,D) -termEq -respecting

then reconsider ss = a as termal Element of S ;

per cases ( ss is literal or not ss is literal ) ;

suppose ss is literal ; :: thesis: X -freeInterpreter a is (X,D) -termEq -respecting

then reconsider l = ss as literal Element of S ;
{(R#2 S),(R#3b S)} c= D by A2;
then X -freeInterpreter l is (X,D) -termEq -respecting by Lm42, A1;
hence X -freeInterpreter a is (X,D) -termEq -respecting ; :: thesis: verum

end;

suppose not ss is literal ; :: thesis: X -freeInterpreter a is (X,D) -termEq -respecting

then reconsider sss = ss as low-compounding Element of S ;
X -freeInterpreter sss is (X,D) -termEq -respecting by Lm38, A1;
hence X -freeInterpreter a is (X,D) -termEq -respecting ; :: thesis: verum

end;

end;

end;

suppose a is relational ; :: thesis: X -freeInterpreter a is (X,D) -termEq -respecting

then reconsider r = a as relational Element of S ;
X -freeInterpreter r is (X,D) -termEq -respecting by Lm41, A1;
hence X -freeInterpreter a is (X,D) -termEq -respecting ; :: thesis: verum

end;

end;