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 monotonic holds
P .. (E (/\) T) c= (P .. E) (/\) (P .. T)