let X be set ; :: thesis: for S being Language
for D being RuleSet of S st {(R0 S),(R3a S)} c= D & {(R2 S),(R3b 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 {(R0 S),(R3a S)} c= D & {(R2 S),(R3b S)} c= D & X is D -expanded holds
(X,D) -termEq is Equivalence_Relation of (AllTermsOf S)
let D be RuleSet of S; :: thesis: ( {(R0 S),(R3a S)} c= D & {(R2 S),(R3b S)} c= D & X is D -expanded implies (X,D) -termEq is Equivalence_Relation of (AllTermsOf S) )
B0: ( {(R2 S)} c= {(R2 S),(R3b S)} & {(R3b S)} c= {(R2 S),(R3b S)} ) by ZFMISC_1:7;
assume {(R0 S),(R3a S)} c= D ; :: thesis: ( not {(R2 S),(R3b S)} c= D or not X is D -expanded or (X,D) -termEq is Equivalence_Relation of (AllTermsOf S) )
then B1: {(R0 S)} \/ {(R3a S)} c= D by ENUMSET1:1;
assume {(R2 S),(R3b S)} c= D ; :: thesis: ( not X is D -expanded or (X,D) -termEq is Equivalence_Relation of (AllTermsOf S) )
then B2: ( {(R2 S)} /\ D = {(R2 S)} & {(R3b S)} /\ D = {(R3b S)} ) by B0, XBOOLE_1:1, XBOOLE_1:28;
assume B3: 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 Lm24, Lm26, B1, B3, Lm25, B2; :: thesis: verum