let X be set ; :: thesis: for S being Language
for a being ofAtomicFormula Element of S
for D being RuleSet of S st {(R0 S),(R3a S)} c= D & D /\ {(R3d S)} = {(R3d S)} & {(R2 S)} /\ D = {(R2 S)} & {(R3b S)} /\ D = {(R3b S)} & D /\ {(R3e S)} = {(R3e 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 {(R0 S),(R3a S)} c= D & D /\ {(R3d S)} = {(R3d S)} & {(R2 S)} /\ D = {(R2 S)} & {(R3b S)} /\ D = {(R3b S)} & D /\ {(R3e S)} = {(R3e 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 {(R0 S),(R3a S)} c= D & D /\ {(R3d S)} = {(R3d S)} & {(R2 S)} /\ D = {(R2 S)} & {(R3b S)} /\ D = {(R3b S)} & D /\ {(R3e S)} = {(R3e S)} & X is D -expanded holds
X -freeInterpreter a is (X,D) -termEq -respecting
let D be RuleSet of S; :: thesis: ( {(R0 S),(R3a S)} c= D & D /\ {(R3d S)} = {(R3d S)} & {(R2 S)} /\ D = {(R2 S)} & {(R3b S)} /\ D = {(R3b S)} & D /\ {(R3e S)} = {(R3e 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 = abs (ar a);
set f = a -compound ;
set R = (X,D) -termEq ;
assume B0: ( {(R0 S),(R3a S)} c= D & D /\ {(R3d S)} = {(R3d S)} & {(R2 S)} /\ D = {(R2 S)} & {(R3b S)} /\ D = {(R3b S)} & D /\ {(R3e S)} = {(R3e S)} & X is D -expanded ) ; :: thesis: X -freeInterpreter a is (X,D) -termEq -respecting
then reconsider S2 = {(R2 S)}, S3 = {(R3b S)} as Subset of D ;
BB1: 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 ;
{(R2 S),(R3b S)} c= D by BB1, ENUMSET1:1;
then X -freeInterpreter l is (X,D) -termEq -respecting by Lm52, B0;
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 Lm48, B0;
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 Lm51, B0;
hence X -freeInterpreter a is (X,D) -termEq -respecting ; :: thesis: verum

end;

end;