let X be set ; for S being Language
for l being literal Element of S
for D being RuleSet of S st {(R#3a S)} c= D & {(R#2 S),(R#3b S)} c= D & X is D -expanded holds
X -freeInterpreter l is (X,D) -termEq -respecting
let S be Language; for l being literal Element of S
for D being RuleSet of S st {(R#3a S)} c= D & {(R#2 S),(R#3b S)} c= D & X is D -expanded holds
X -freeInterpreter l is (X,D) -termEq -respecting
let l be literal Element of S; for D being RuleSet of S st {(R#3a S)} c= D & {(R#2 S),(R#3b S)} c= D & X is D -expanded holds
X -freeInterpreter l is (X,D) -termEq -respecting
let D be RuleSet of S; ( {(R#3a S)} c= D & {(R#2 S),(R#3b S)} c= D & X is D -expanded implies X -freeInterpreter l is (X,D) -termEq -respecting )
set AT = AllTermsOf S;
set I = X -freeInterpreter l;
assume
( {(R#3a S)} c= D & {(R#2 S),(R#3b S)} c= D & X is D -expanded )
; X -freeInterpreter l is (X,D) -termEq -respecting
then reconsider R = (X,D) -termEq as Equivalence_Relation of (AllTermsOf S) by Lm34;
X -freeInterpreter l is R -respecting
by FOMODEL3:18;
hence
X -freeInterpreter l is (X,D) -termEq -respecting
; verum