let X be set ; :: thesis: for S being Language
for D being RuleSet of S st {(R#3a S)} c= D & X is D -expanded holds
(X,D) -termEq is transitive
let S be Language; :: thesis: for D being RuleSet of S st {(R#3a S)} c= D & X is D -expanded holds
(X,D) -termEq is transitive
let D be RuleSet of S; :: thesis: ( {(R#3a S)} c= D & X is D -expanded implies (X,D) -termEq is transitive )
set AT = AllTermsOf S;
set E = TheEqSymbOf S;
set Q = S -sequents ;
set AF = AllFormulasOf S;
set E3 = R#3a S;
set R = (X,D) -termEq ;
set G3 = {(R#3a S)};
assume A1: {(R#3a S)} c= D ; :: thesis: ( not X is D -expanded or (X,D) -termEq is transitive )
then reconsider DD = D as non empty RuleSet of S ;
reconsider GG3 = {(R#3a S)} as non empty Subset of DD by A1;
assume A2: X is D -expanded ; :: thesis: (X,D) -termEq is transitive
A3: field ((X,D) -termEq) c= (AllTermsOf S) \/ (AllTermsOf S) by RELSET_1:8;

now :: thesis: for x, y, z being object st x in field ((X,D) -termEq) & y in field ((X,D) -termEq) & z in field ((X,D) -termEq) & [x,y] in (X,D) -termEq & [y,z] in (X,D) -termEq holds
[x,z] in (X,D) -termEq

let x, y, z be object ; :: thesis: ( x in field ((X,D) -termEq) & y in field ((X,D) -termEq) & z in field ((X,D) -termEq) & [x,y] in (X,D) -termEq & [y,z] in (X,D) -termEq implies [x,z] in (X,D) -termEq )
assume ( x in field ((X,D) -termEq) & y in field ((X,D) -termEq) & z in field ((X,D) -termEq) ) ; :: thesis: ( [x,y] in (X,D) -termEq & [y,z] in (X,D) -termEq implies [x,z] in (X,D) -termEq )
then reconsider tt1 = x, tt2 = y, tt3 = z as Element of AllTermsOf S by A3;
reconsider t1 = tt1, t2 = tt2, t3 = tt3 as termal string of S ;
set phi1 = (<*(TheEqSymbOf S)*> ^ t1) ^ t2;
set phi2 = (<*(TheEqSymbOf S)*> ^ t2) ^ t3;
set phi3 = (<*(TheEqSymbOf S)*> ^ t1) ^ t3;
assume ( [x,y] in (X,D) -termEq & [y,z] in (X,D) -termEq ) ; :: thesis: [x,z] in (X,D) -termEq
then A4: ( (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is X,D -provable & (<*(TheEqSymbOf S)*> ^ t2) ^ t3 is X,D -provable ) by Lm23;
reconsider XX = X as non empty set by A2, A4;
reconsider phi11 = (<*(TheEqSymbOf S)*> ^ t1) ^ t2, phi22 = (<*(TheEqSymbOf S)*> ^ t2) ^ t3 as Element of XX by A4, A2;
reconsider Phi = {phi11,phi22} as non empty Subset of XX ;
[{((<*(TheEqSymbOf S)*> ^ t1) ^ t2),((<*(TheEqSymbOf S)*> ^ t2) ^ t3)},((<*(TheEqSymbOf S)*> ^ t1) ^ t3)] is 1, {} ,{(R#3a S)} -derivable ;
then ( [Phi,((<*(TheEqSymbOf S)*> ^ t1) ^ t3)] is 1, {} ,{(R#3a S)} -derivable & GG3 c= D ) ;
then [Phi,((<*(TheEqSymbOf S)*> ^ t1) ^ t3)] is 1, {} ,DD -derivable by Th2;
then (<*(TheEqSymbOf S)*> ^ t1) ^ t3 is X,DD -provable ;
hence [x,z] in (X,D) -termEq ; :: thesis: verum

end;

hence (X,D) -termEq is transitive by RELAT_2:def 8, RELAT_2:def 16; :: thesis: verum