defpred S₁[ SortSymbol of S, set , set ] means $2,$3 are_convertible_wrt (TRS R) . $1;
consider P being ManySortedRelation of the Sorts of A such that
A5: for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in P . s iff S₁[s,a,b] ) from MSUALG_6:sch 2();
reconsider P = P as ManySortedRelation of A ;
reconsider P = P as EquationalTheory of A by A5, Th50;
take P ; :: thesis: ( R c= P & ( for Q being EquationalTheory of A st R c= Q holds
P c= Q ) )
thus R c= P :: thesis: for Q being EquationalTheory of A st R c= Q holds
P c= Q

proof

let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in the carrier of S or R . i c= P . i )
assume i in the carrier of S ; :: thesis: R . i c= P . i
then reconsider s = i as SortSymbol of S ;
R . s c= P . s

proof

let x, y be set ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in R . s or [x,y] in P . s )
assume A6: [x,y] in R . s ; :: thesis: [x,y] in P . s
then reconsider a = x, b = y as Element of A,s by ZFMISC_1:106;
R c= TRS R by Def13;
then R . s c= (TRS R) . s by PBOOLE:def 5;
then a,b are_convertible_wrt (TRS R) . s by A6, REWRITE1:30;
hence [x,y] in P . s by A5; :: thesis: verum

end;

hence R . i c= P . i ; :: thesis: verum

end;

let Q be EquationalTheory of A; :: thesis: ( R c= Q implies P c= Q )
assume R c= Q ; :: thesis: P c= Q
then A7: TRS R c= Q by Def13;
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in the carrier of S or P . i c= Q . i )
assume i in the carrier of S ; :: thesis: P . i c= Q . i
then reconsider s = i as SortSymbol of S ;
P . s c= Q . s

proof

let x, y be set ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in P . s or [x,y] in Q . s )
assume A8: [x,y] in P . s ; :: thesis: [x,y] in Q . s
then reconsider a = x, b = y as Element of A,s by ZFMISC_1:106;
( Q is MSEquivalence_Relation-like & a,b are_convertible_wrt (TRS R) . s ) by A5, A8;
hence [x,y] in Q . s by A7, Th51; :: thesis: verum

end;

hence P . i c= Q . i ; :: thesis: verum