:: deftheorem defines Full CLOSURE2:def 20 :
for S being 1-sorted
for MS being many-sorted over S holds Full MS = ClosureStr(# the Sorts of MS,(Bool the Sorts of MS) #);