let X be set ; :: thesis: for S being Language
for D being RuleSet of S st D is 0 -ranked & X is D -expanded holds
(X,D) -termEq is Equivalence_Relation of (AllTermsOf S)
let S be Language; :: thesis: for D being RuleSet of S st D is 0 -ranked & X is D -expanded holds
(X,D) -termEq is Equivalence_Relation of (AllTermsOf S)
let D be RuleSet of S; :: thesis: ( D is 0 -ranked & X is D -expanded implies (X,D) -termEq is Equivalence_Relation of (AllTermsOf S) )
assume D is 0 -ranked ; :: thesis: ( not X is D -expanded or (X,D) -termEq is Equivalence_Relation of (AllTermsOf S) )
then ( R#0 S in D & R#3a S in D & R#2 S in D & R#3b S in D ) by Def62;
then ( {(R#0 S)} c= D & {(R#3a S)} c= D & {(R#2 S)} c= D & {(R#3b S)} c= D ) by ZFMISC_1:31;
then A1: ( {(R#3a S)} c= D & {(R#2 S),(R#3b S)} c= D ) by XBOOLE_1:8;
assume X is D -expanded ; :: thesis: (X,D) -termEq is Equivalence_Relation of (AllTermsOf S)
hence (X,D) -termEq is Equivalence_Relation of (AllTermsOf S) by A1, Lm34; :: thesis: verum