let X be set ; :: thesis: for S being Language
for D being RuleSet of S st {(R0 S)} \/ {(R3a 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 {(R0 S)} \/ {(R3a S)} c= D & X is D -expanded holds
(X,D) -termEq is transitive
let D be RuleSet of S; :: thesis: ( {(R0 S)} \/ {(R3a 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 Phi = X;
set R = (X,D) -termEq ;
reconsider Seqts = {} as Element of bool (S -sequents) by XBOOLE_1:2;
assume B7: {(R0 S)} \/ {(R3a S)} c= D ; :: thesis: ( not X is D -expanded or (X,D) -termEq is transitive )
assume B6: X is D -expanded ; :: thesis: (X,D) -termEq is transitive
B9: field ((X,D) -termEq) c= (AllTermsOf S) \/ (AllTermsOf S) by RELSET_1:8;

now

let x, y, z be set ; :: 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 B9;
reconsider t1 = tt1, t2 = tt2, t3 = tt3 as termal string of S ;
reconsider phi1 = (<*(TheEqSymbOf S)*> ^ t1) ^ t2 as wff string of S by Lm10;
reconsider phi2 = (<*(TheEqSymbOf S)*> ^ t2) ^ t3 as wff string of S by Lm10;
reconsider phi3 = (<*(TheEqSymbOf S)*> ^ t1) ^ t3 as wff string of S by Lm10;
[{phi1,((<*(TheEqSymbOf S)*> ^ t2) ^ t3)},((<*(TheEqSymbOf S)*> ^ t1) ^ t3)] is 1,{[{phi1},((<*(TheEqSymbOf S)*> ^ t1) ^ t2)]},{(R3a S)} -derivable ;
then B2: [{phi1,phi2},phi3] is 1,{[{phi1},phi1]},{(R3a S)} -derivable ;
[{phi1,phi2},phi3] is 1 + 1, {} ,{(R0 S)} \/ {(R3a S)} -derivable by B2, Lm28;
then {[{phi1,phi2},phi3]} is {} ,{(R0 S)} \/ {(R3a S)} -derivable by Lm29;
then {[{phi1,phi2},phi3]} is {} ,D -derivable by Lm20, B7;
then BB3: ( {phi1,phi2} = {phi1} \/ {phi2} & phi3 is {phi1,phi2},D -provable ) by DefProvable, ENUMSET1:1;
assume ( [x,y] in (X,D) -termEq & [y,z] in (X,D) -termEq ) ; :: thesis: [x,z] in (X,D) -termEq
then ( phi1 is X,D -provable & phi2 is X,D -provable ) by Lm23;
then reconsider Phi1 = {phi1}, Phi2 = {phi2} as Subset of X by B6, DefExpanded;
reconsider Phi3 = Phi1 \/ Phi2 as Subset of X ;
phi3 is Phi3,D -provable by BB3;
hence [x,z] in (X,D) -termEq ; :: thesis: verum

end;

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