:: deftheorem defines MSFull CLOSURE1:def 11 :
for S being 1-sorted
for MS being many-sorted over S holds MSFull MS = MSClosureStr(# the Sorts of MS,(bool the Sorts of MS) #);