let X be set ; :: thesis: for S being Language
for D being RuleSet of S st {(R#3b S)} c= D & X is D -expanded holds
(X,D) -termEq is symmetric
let S be Language; :: thesis: for D being RuleSet of S st {(R#3b S)} c= D & X is D -expanded holds
(X,D) -termEq is symmetric
let D be RuleSet of S; :: thesis: ( {(R#3b S)} c= D & X is D -expanded implies (X,D) -termEq is symmetric )
set AT = AllTermsOf S;
set E = TheEqSymbOf S;
set Q = S -sequents ;
set AF = AllFormulasOf S;
set Phi = X;
set R = (X,D) -termEq ;
assume A1: {(R#3b S)} c= D ; :: thesis: ( not X is D -expanded or (X,D) -termEq is symmetric )
assume A2: X is D -expanded ; :: thesis: (X,D) -termEq is symmetric
A3: field ((X,D) -termEq) c= (AllTermsOf S) \/ (AllTermsOf S) by RELSET_1:8;

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

let x, y be object ; :: thesis: ( x in field ((X,D) -termEq) & y in field ((X,D) -termEq) & [x,y] in (X,D) -termEq implies [y,x] in (X,D) -termEq )
assume ( x in field ((X,D) -termEq) & y in field ((X,D) -termEq) ) ; :: thesis: ( [x,y] in (X,D) -termEq implies [y,x] in (X,D) -termEq )
then reconsider tt1 = x, tt2 = y as Element of AllTermsOf S by A3;
reconsider t1 = tt1, t2 = tt2 as termal string of S ;
reconsider phi1 = (<*(TheEqSymbOf S)*> ^ t1) ^ t2 as wff string of S ;
reconsider phi2 = (<*(TheEqSymbOf S)*> ^ t2) ^ t1 as wff string of S ;
reconsider seqt = [{phi1},phi2] as Element of S -sequents by Def2;
reconsider Seqts = {} as Element of bool (S -sequents) by XBOOLE_1:2;
A5: seqt Rule3b {} ;
[Seqts,seqt] in P#3b S by A5, Def38;
then seqt in (R#3b S) . Seqts by Lm27;
then {seqt} is {} ,{(R#3b S)} -derivable by Lm20, ZFMISC_1:31;
then {seqt} is {} ,D -derivable by A1, Lm18;
then A6: phi2 is {phi1},D -provable ;
assume [x,y] in (X,D) -termEq ; :: thesis: [y,x] in (X,D) -termEq
then consider t11, t22 being termal string of S such that
A7: ( [x,y] = [t11,t22] & (<*(TheEqSymbOf S)*> ^ t11) ^ t22 is X,D -provable ) ;
( t1 = t11 & t2 = t22 ) by XTUPLE_0:1, A7;
then {phi1} c= X by A2, A7;
hence [y,x] in (X,D) -termEq by A6; :: thesis: verum

end;

hence (X,D) -termEq is symmetric by RELAT_2:def 3, RELAT_2:def 11; :: thesis: verum