let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of 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 (TRS R) . s iff ex s' being SortSymbol of S st
( TranslationRel S reduces s',s & ex l, r being Element of A,s' ex h being Endomorphism of A ex t being Translation of A,s',s st
( [l,r] in R . s' & a = t . ((h . s') . l) & b = t . ((h . s') . r) ) ) )
let A be non-empty MSAlgebra of 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 (TRS R) . s iff ex s' being SortSymbol of S st
( TranslationRel S reduces s',s & ex l, r being Element of A,s' ex h being Endomorphism of A ex t being Translation of A,s',s st
( [l,r] in R . s' & a = t . ((h . s') . l) & b = t . ((h . s') . r) ) ) )
let R 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 (TRS R) . s iff ex s' being SortSymbol of S st
( TranslationRel S reduces s',s & ex l, r being Element of A,s' ex h being Endomorphism of A ex t being Translation of A,s',s st
( [l,r] in R . s' & a = t . ((h . s') . l) & b = t . ((h . s') . r) ) ) )
let s be SortSymbol of S; :: thesis: for a, b being Element of A,s holds
( [a,b] in (TRS R) . s iff ex s' being SortSymbol of S st
( TranslationRel S reduces s',s & ex l, r being Element of A,s' ex h being Endomorphism of A ex t being Translation of A,s',s st
( [l,r] in R . s' & a = t . ((h . s') . l) & b = t . ((h . s') . r) ) ) )
let a, b be Element of A,s; :: thesis: ( [a,b] in (TRS R) . s iff ex s' being SortSymbol of S st
( TranslationRel S reduces s',s & ex l, r being Element of A,s' ex h being Endomorphism of A ex t being Translation of A,s',s st
( [l,r] in R . s' & a = t . ((h . s') . l) & b = t . ((h . s') . r) ) ) )
A1: InvCl (StabCl R) = TRS R by Th37;

hereby :: thesis: ( ex s' being SortSymbol of S st
( TranslationRel S reduces s',s & ex l, r being Element of A,s' ex h being Endomorphism of A ex t being Translation of A,s',s st
( [l,r] in R . s' & a = t . ((h . s') . l) & b = t . ((h . s') . r) ) ) implies [a,b] in (TRS R) . s )

assume [a,b] in (TRS R) . s ; :: thesis: ex s' being SortSymbol of S st
( TranslationRel S reduces s',s & ex u, v being Element of A,s' ex h being Endomorphism of A ex t being Translation of A,s',s st
( [u,v] in R . s' & a = t . ((h . s') . u) & b = t . ((h . s') . v) ) )
then consider s' being SortSymbol of S, x, y being Element of A,s', t being Translation of A,s',s such that
A2: ( TranslationRel S reduces s',s & [x,y] in (StabCl R) . s' & a = t . x & b = t . y ) by A1, Th29;
take s' = s'; :: thesis: ( TranslationRel S reduces s',s & ex u, v being Element of A,s' ex h being Endomorphism of A ex t being Translation of A,s',s st
( [u,v] in R . s' & a = t . ((h . s') . u) & b = t . ((h . s') . v) ) )
thus TranslationRel S reduces s',s by A2; :: thesis: ex u, v being Element of A,s' ex h being Endomorphism of A ex t being Translation of A,s',s st
( [u,v] in R . s' & a = t . ((h . s') . u) & b = t . ((h . s') . v) )
consider u, v being Element of A,s', h being Endomorphism of A such that
A3: ( [u,v] in R . s' & x = (h . s') . u & y = (h . s') . v ) by A2, Th31;
take u = u; :: thesis: ex v being Element of A,s' ex h being Endomorphism of A ex t being Translation of A,s',s st
( [u,v] in R . s' & a = t . ((h . s') . u) & b = t . ((h . s') . v) )
take v = v; :: thesis: ex h being Endomorphism of A ex t being Translation of A,s',s st
( [u,v] in R . s' & a = t . ((h . s') . u) & b = t . ((h . s') . v) )
take h = h; :: thesis: ex t being Translation of A,s',s st
( [u,v] in R . s' & a = t . ((h . s') . u) & b = t . ((h . s') . v) )
reconsider t = t as Translation of A,s',s ;
take t = t; :: thesis: ( [u,v] in R . s' & a = t . ((h . s') . u) & b = t . ((h . s') . v) )
thus ( [u,v] in R . s' & a = t . ((h . s') . u) & b = t . ((h . s') . v) ) by A2, A3; :: thesis: verum

end;

given s' being SortSymbol of S such that A4: TranslationRel S reduces s',s and
A5: ex l, r being Element of A,s' ex h being Endomorphism of A ex t being Translation of A,s',s st
( [l,r] in R . s' & a = t . ((h . s') . l) & b = t . ((h . s') . r) ) ; :: thesis: [a,b] in (TRS R) . s
consider l, r being Element of A,s', h being Endomorphism of A, t being Translation of A,s',s such that
A6: ( [l,r] in R . s' & a = t . ((h . s') . l) & b = t . ((h . s') . r) ) by A5;
[((h . s') . l),((h . s') . r)] in (StabCl R) . s' by A6, Th31;
hence [a,b] in (TRS R) . s by A1, A4, A6, Th29; :: thesis: verum