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 ( R0 S in D & R3a S in D & R2 S in D & R3b S in D ) by DefRank;
then ( {(R0 S)} c= D & {(R3a S)} c= D & {(R2 S)} c= D & {(R3b S)} c= D ) by ZFMISC_1:31;
then ( {(R0 S)} \/ {(R3a S)} c= D & {(R2 S)} \/ {(R3b S)} c= D ) by XBOOLE_1:8;
then B1: ( {(R0 S),(R3a S)} c= D & {(R2 S),(R3b S)} c= D ) by ENUMSET1:1;
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 B1, Lm11; :: thesis: verum