let X be set ; :: thesis: for S being Language
for a being ofAtomicFormula Element of S
for D being RuleSet of S st D is 1 -ranked & 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 D is 1 -ranked & 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 D is 1 -ranked & X is D -expanded holds
X -freeInterpreter a is (X,D) -termEq -respecting
let D be RuleSet of S; :: thesis: ( D is 1 -ranked & X is D -expanded implies X -freeInterpreter a is (X,D) -termEq -respecting )
assume A1: D is 1 -ranked ; :: thesis: ( not X is D -expanded or X -freeInterpreter a is (X,D) -termEq -respecting )
then ( R#0 S in D & R#3a S in D ) by Def59;
then ( {(R#0 S)} c= D & {(R#3a S)} c= D ) by ZFMISC_1:31;
then {(R#0 S)} \/ {(R#3a S)} c= D by XBOOLE_1:8;
then A2: {(R#0 S),(R#3a S)} c= D by ENUMSET1:1;
( R#3d S in D & R#2 S in D & R#3b S in D & R#3e S in D ) by A1, Def59;
then ( {(R#3d S)} c= D & {(R#2 S)} c= D & {(R#3b S)} c= D & {(R#3e S)} c= D ) by ZFMISC_1:31;
then A3: ( D /\ {(R#3d S)} = {(R#3d S)} & D /\ {(R#2 S)} = {(R#2 S)} & D /\ {(R#3b S)} = {(R#3b S)} & D /\ {(R#3e S)} = {(R#3e S)} ) by XBOOLE_1:28;
assume X is D -expanded ; :: thesis: X -freeInterpreter a is (X,D) -termEq -respecting
hence X -freeInterpreter a is (X,D) -termEq -respecting by Lm45, A2, A3; :: thesis: verum