let X be set ; :: thesis: for S being Language
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,D) -termEq is Equivalence_Relation of (AllTermsOf S)
let S be Language; :: thesis: 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,D) -termEq is Equivalence_Relation of (AllTermsOf S)
let D be RuleSet of S; :: thesis: ( {(R#3a S)} c= D & {(R#2 S),(R#3b S)} c= D & X is D -expanded implies (X,D) -termEq is Equivalence_Relation of (AllTermsOf S) )
A1: ( {(R#2 S)} c= {(R#2 S),(R#3b S)} & {(R#3b S)} c= {(R#2 S),(R#3b S)} ) by ZFMISC_1:7;
assume A2: {(R#3a S)} c= D ; :: thesis: ( not {(R#2 S),(R#3b S)} c= D or not X is D -expanded or (X,D) -termEq is Equivalence_Relation of (AllTermsOf S) )
assume A3: {(R#2 S),(R#3b S)} c= D ; :: thesis: ( not X is D -expanded or (X,D) -termEq is Equivalence_Relation of (AllTermsOf S) )
assume A4: X is D -expanded ; :: thesis: (X,D) -termEq is Equivalence_Relation of (AllTermsOf S)
thus (X,D) -termEq is Equivalence_Relation of (AllTermsOf S) by Lm31, Lm33, A2, A4, Lm32, A3, A1, XBOOLE_1:1; :: thesis: verum