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