for I being set
for M being ManySortedSet of I
for E, T being Element of Bool M
for g being SetOp of M
for A being Element of Bool M st A = E (/\) T & g is monotonic holds
g . A c= (g . E) (/\) (g . T)