theorem :: CLOSURE1:19

for I being set
for M being ManySortedSet of I
for P being MSSetOp of M
for E, T being Element of bool M st P is topological holds
(P .. E) (\) (P .. T) c= P .. (E (\) T)