let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for R being invariant ManySortedRelation of A holds InvCl R = R
let A be non-empty MSAlgebra over S; :: thesis: for R being invariant ManySortedRelation of A holds InvCl R = R
let R be invariant ManySortedRelation of A; :: thesis: InvCl R = R
( InvCl R c= R & R c= InvCl R ) by Def11;
hence InvCl R = R by PBOOLE:146; :: thesis: verum