:: deftheorem defines support CLOSURE3:def 1 :
for I being non empty set
for M being ManySortedSet of I holds support M = { x where x is Element of I : M . x <> {} } ;