:: deftheorem Def11 defines InvCl MSUALG_6:def 11 :
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 b₄ being invariant ManySortedRelation of A holds
( b₄ = InvCl R iff ( R c= b₄ & ( for Q being invariant ManySortedRelation of A st R c= Q holds
b₄ c= Q ) ) );