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 holds
( StabCl R c= TRS R & InvCl R c= TRS R & StabCl (InvCl R) c= TRS R )