defpred S₁[ Function, SortSymbol of , SortSymbol of ] means ( TranslationRel S reduces $2,$3 & $1 is Translation of A,$2,$3 );
defpred S₂[ SortSymbol of , set , set ] means ex s' being SortSymbol of ex f being Function of the Sorts of A . s',the Sorts of A . $1 ex x, y being Element of A,s' st
( S₁[f,s',$1] & [x,y] in R . s' & $2 = f . x & $3 = f . y );
consider Q being ManySortedRelation of the Sorts of A such that
A5: for s being SortSymbol of
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