defpred S₁[ Function, SortSymbol of S, SortSymbol of S] means ( TranslationRel S reduces $2,$3 & $1 is Translation of A,$2,$3 );
defpred S₂[ SortSymbol of S, set , set ] means ex s9 being SortSymbol of S ex f being Function of ( the Sorts of A . s9),( the Sorts of A . $1) ex x, y being Element of A,s9 st
( S₁[f,s9,$1] & [x,y] in R . s9 & $2 = f . x & $3 = f . y );
consider Q 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 Q . s iff S₂[s,a,b] ) from MSUALG_6:sch 2();
reconsider Q = Q as ManySortedRelation of A ;
reconsider Q = Q as invariant ManySortedRelation of A by A5, Lm1;
take Q ; :: thesis: ( R c= Q & ( for Q being invariant ManySortedRelation of A st R c= Q holds
Q c= Q ) )
thus ( R c= Q & ( for Q being invariant ManySortedRelation of A st R c= Q holds
Q c= Q ) ) by A5, Lm1; :: thesis: verum