:: deftheorem Def8 defines invariant MSUALG_6:def 8 :
for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for R being ManySortedRelation of A holds
( R is invariant iff for s1, s2 being SortSymbol of S
for t being Function st t is_e.translation_of A,s1,s2 holds
for a, b being set st [a,b] in R . s1 holds
[(t . a),(t . b)] in R . s2 );