reconsider SS = the Sorts of MA as ManySortedSet of the carrier of 1-sorted(# the carrier of S #) ;
SubSort MA c= Bool the Sorts of MA

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in SubSort MA or x in Bool the Sorts of MA )
assume x in SubSort MA ; :: thesis: x in Bool the Sorts of MA
then x is ManySortedSubset of the Sorts of MA by MSUALG_2:def 11;
hence x in Bool the Sorts of MA by CLOSURE2:def 1; :: thesis: verum

end;

then reconsider SF = SubSort MA as SubsetFamily of SS ;
take ClosureStr(# SS,SF #) ; :: thesis: ( the Sorts of ClosureStr(# SS,SF #) = the Sorts of MA & the Family of ClosureStr(# SS,SF #) = SubSort MA )
thus ( the Sorts of ClosureStr(# SS,SF #) = the Sorts of MA & the Family of ClosureStr(# SS,SF #) = SubSort MA ) ; :: thesis: verum