:: deftheorem defines topological CLOSURE1:def 4 :
for I being set
for M being ManySortedSet of I
for IT being MSSetOp of M holds
( IT is topological iff for X, Y being Element of bool M holds IT .. (X (\/) Y) = (IT .. X) (\/) (IT .. Y) );