let X be set ; :: thesis: for S being Language
for D being RuleSet of S st {(R2 S)} c= D holds
(X,D) -termEq is total
let S be Language; :: thesis: for D being RuleSet of S st {(R2 S)} c= D holds
(X,D) -termEq is total
let D be RuleSet of S; :: thesis: ( {(R2 S)} c= D implies (X,D) -termEq is total )
assume B0: {(R2 S)} c= D ; :: thesis: (X,D) -termEq is total
set AT = AllTermsOf S;
set E = TheEqSymbOf S;
set Phi = X;
set R = (X,D) -termEq ;

now

let x be set ; :: thesis: ( x in AllTermsOf S implies x in dom ((X,D) -termEq) )
assume x in AllTermsOf S ; :: thesis: x in dom ((X,D) -termEq)
then reconsider t = x as termal string of S ;
set phi = (<*(TheEqSymbOf S)*> ^ t) ^ t;
set seqt = [{},((<*(TheEqSymbOf S)*> ^ t) ^ t)];
{[{},((<*(TheEqSymbOf S)*> ^ t) ^ t)]} is {} ,D -derivable by B0, Lm20;
then (<*(TheEqSymbOf S)*> ^ t) ^ t is {} \ (X \ {}),D -provable by DefProvable;
then (<*(TheEqSymbOf S)*> ^ t) ^ t is X \/ {},D -provable ;
then [t,t] in (X,D) -termEq ;
hence x in dom ((X,D) -termEq) by RELAT_1:def 4; :: thesis: verum

end;

then AllTermsOf S c= dom ((X,D) -termEq) by TARSKI:def 3;
then AllTermsOf S = dom ((X,D) -termEq) by XBOOLE_0:def 10;
hence (X,D) -termEq is total by PARTFUN1:def 2; :: thesis: verum