let I be set ; :: thesis: 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)
let M be ManySortedSet of I; :: thesis: 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)
let P be MSSetOp of M; :: thesis: for E, T being Element of bool M st P is monotonic holds
P .. (E /\ T) c= (P .. E) /\ (P .. T)
let E, T be Element of bool M; :: thesis: ( P is monotonic implies P .. (E /\ T) c= (P .. E) /\ (P .. T) )
assume A1: P is monotonic ; :: thesis: P .. (E /\ T) c= (P .. E) /\ (P .. T)
E in bool M by MSSUBFAM:12;
then E c= M by MBOOLEAN:1;
then E /\ T c= M by MBOOLEAN:14;
then E /\ T in bool M by MBOOLEAN:1;
then A2: E /\ T is Element of bool M by MSSUBFAM:11;
E /\ T c= T by PBOOLE:15;
then A3: P .. (E /\ T) c= P .. T by A1, A2, Def3;
E /\ T c= E by PBOOLE:15;
then P .. (E /\ T) c= P .. E by A1, A2, Def3;
hence P .. (E /\ T) c= (P .. E) /\ (P .. T) by A3, PBOOLE:17; :: thesis: verum