:: deftheorem defines topological CLOSURE2:def 13 :
for I being set
for M being ManySortedSet of I
for IT being SetOp of M holds
( IT is topological iff for x, y being Element of Bool M holds IT . (x (\/) y) = (IT . x) (\/) (IT . y) );