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 object ; :: according to PBOOLE:def 2 :: 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 object ; :: 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:87;
R c= TRS R by Def13;
then R . s c= (TRS R) . s ;
then a,b are_convertible_wrt (TRS R) . s by A6, REWRITE1:29;
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 A7: R c= Q ; :: thesis: P c= Q
let i be object ; :: according to PBOOLE:def 2 :: 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 ;
A8: TRS R c= Q by A7, Def13;
P . s c= Q . s

proof

let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in P . s or [x,y] in Q . s )
assume A9: [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:87;
a,b are_convertible_wrt (TRS R) . s by A5, A9;
hence [x,y] in Q . s by A8, Th51; :: thesis: verum

end;

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