theorem Th29: :: MSUALG_6:29

for S being non empty non void ManySortedSign
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 ) )