let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for R being ManySortedRelation of the Sorts of A
for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in (InvCl R) . s iff ex s9 being SortSymbol of S ex x, y being Element of A,s9 ex t being Translation of A,s9,s st
( TranslationRel S reduces s9,s & [x,y] in R . s9 & a = t . x & b = t . y ) )
let A be non-empty MSAlgebra over S; :: thesis: for R being ManySortedRelation of the Sorts of A
for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in (InvCl R) . s iff ex s9 being SortSymbol of S ex x, y being Element of A,s9 ex t being Translation of A,s9,s st
( TranslationRel S reduces s9,s & [x,y] in R . s9 & a = t . x & b = t . y ) )
let P be ManySortedRelation of the Sorts of A; :: thesis: for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in (InvCl P) . s iff ex s9 being SortSymbol of S ex x, y being Element of A,s9 ex t being Translation of A,s9,s st
( TranslationRel S reduces s9,s & [x,y] in P . s9 & a = t . x & b = t . y ) )
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
( TranslationRel S reduces s9,$1 & f is Translation of A,s9,$1 & [x,y] in P . s9 & $2 = f . x & $3 = f . y );
let s be SortSymbol of S; :: thesis: for a, b being Element of A,s holds
( [a,b] in (InvCl P) . s iff ex s9 being SortSymbol of S ex x, y being Element of A,s9 ex t being Translation of A,s9,s st
( TranslationRel S reduces s9,s & [x,y] in P . s9 & a = t . x & b = t . y ) )
let a, b be Element of A,s; :: thesis: ( [a,b] in (InvCl P) . s iff ex s9 being SortSymbol of S ex x, y being Element of A,s9 ex t being Translation of A,s9,s st
( TranslationRel S reduces s9,s & [x,y] in P . s9 & a = t . x & b = t . y ) )
consider Q being ManySortedRelation of the Sorts of A such that
A1: 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 R = P, Q = Q as ManySortedRelation of A ;
A2: R c= Q by A1, Lm1;
reconsider Q = Q as invariant ManySortedRelation of A by A1, Lm1;
R c= InvCl R by Def11;
then A3: Q c= InvCl R by A1, Lm1;
InvCl R c= Q by A2, Def11;
then A4: InvCl R = Q by A3, PBOOLE:146;

hereby :: thesis: ( ex s9 being SortSymbol of S ex x, y being Element of A,s9 ex t being Translation of A,s9,s st
( TranslationRel S reduces s9,s & [x,y] in P . s9 & a = t . x & b = t . y ) implies [a,b] in (InvCl P) . s )

assume [a,b] in (InvCl P) . s ; :: thesis: ex s9 being SortSymbol of S ex x, y being Element of A,s9 ex t being Translation of A,s9,s st
( TranslationRel S reduces s9,s & [x,y] in P . s9 & a = t . x & b = t . y )
then ex s9 being SortSymbol of S ex f being Function of ( the Sorts of A . s9),( the Sorts of A . s) ex x, y being Element of A,s9 st
( TranslationRel S reduces s9,s & f is Translation of A,s9,s & [x,y] in P . s9 & a = f . x & b = f . y ) by A1, A4;
hence ex s9 being SortSymbol of S ex x, y being Element of A,s9 ex t being Translation of A,s9,s st
( TranslationRel S reduces s9,s & [x,y] in P . s9 & a = t . x & b = t . y ) ; :: thesis: verum

end;

thus ( ex s9 being SortSymbol of S ex x, y being Element of A,s9 ex t being Translation of A,s9,s st
( TranslationRel S reduces s9,s & [x,y] in P . s9 & a = t . x & b = t . y ) implies [a,b] in (InvCl P) . s ) by A1, A4; :: thesis: verum