let X be set ; :: thesis: for S being Language
for D being RuleSet of S st {(R3b 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 {(R3b S)} c= D & X is D -expanded holds
(X,D) -termEq is symmetric
let D be RuleSet of S; :: thesis: ( {(R3b 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 B7: {(R3b S)} c= D ; :: thesis: ( not X is D -expanded or (X,D) -termEq is symmetric )
assume B6: X is D -expanded ; :: thesis: (X,D) -termEq is symmetric
B9: field ((X,D) -termEq) c= (AllTermsOf S) \/ (AllTermsOf S) by RELSET_1:8;

now

let x, y be set ; :: 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 B9;
reconsider t1 = tt1, t2 = tt2 as termal string of S ;
reconsider phi1 = (<*(TheEqSymbOf S)*> ^ t1) ^ t2 as wff string of S by Lm10;
reconsider phi2 = (<*(TheEqSymbOf S)*> ^ t2) ^ t1 as wff string of S by Lm10;
reconsider seqt = [{phi1},phi2] as Element of S -sequents by DefSeqtLike;
B0: ( seqt `1 = {phi1} & seqt `2 = phi2 ) by MCART_1:7;
reconsider Seqts = {} as Element of bool (S -sequents) by XBOOLE_1:2;
B1: seqt Rule3b {} by B0, Def3b;
[Seqts,seqt] in P3b S by B1, DefP3b;
then seqt in (R3b S) . Seqts by Lm1;
then {seqt} c= (R3b S) . Seqts by ZFMISC_1:31;
then {seqt} is {} ,{(R3b S)} -derivable by Lm9;
then {seqt} is {} ,D -derivable by B7, Lm20;
then B8: phi2 is {phi1},D -provable by DefProvable;
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
B2: ( [x,y] = [t11,t22] & (<*(TheEqSymbOf S)*> ^ t11) ^ t22 is X,D -provable ) ;
( t1 = t11 & t2 = t22 ) by B2, ZFMISC_1:27;
then {phi1} c= X by B6, DefExpanded, B2;
hence [y,x] in (X,D) -termEq by B8; :: thesis: verum

end;

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