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 B0: D is 1 -ranked ; :: thesis: ( not X is D -expanded or X -freeInterpreter a is (X,D) -termEq -respecting )
then ( R0 S in D & R3a S in D ) by DefRank;
then ( {(R0 S)} c= D & {(R3a S)} c= D ) by ZFMISC_1:31;
then {(R0 S)} \/ {(R3a S)} c= D by XBOOLE_1:8;
then B1: {(R0 S),(R3a S)} c= D by ENUMSET1:1;
( R3d S in D & R2 S in D & R3b S in D & R3e S in D ) by B0, DefRank;
then ( {(R3d S)} c= D & {(R2 S)} c= D & {(R3b S)} c= D & {(R3e S)} c= D ) by ZFMISC_1:31;
then B2: ( D /\ {(R3d S)} = {(R3d S)} & D /\ {(R2 S)} = {(R2 S)} & D /\ {(R3b S)} = {(R3b S)} & D /\ {(R3e S)} = {(R3e 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 Lm53, B1, B2; :: thesis: verum