let I be set ; :: thesis: for M being ManySortedSet of I
for P, R being MSSetOp of M st P is monotonic & R is monotonic holds
P ** R is monotonic
let M be ManySortedSet of I; :: thesis: for P, R being MSSetOp of M st P is monotonic & R is monotonic holds
P ** R is monotonic
let P, R be MSSetOp of M; :: thesis: ( P is monotonic & R is monotonic implies P ** R is monotonic )
assume that
A1: P is monotonic and
A2: R is monotonic ; :: thesis: P ** R is monotonic
A3: doms R = bool M by MSSUBFAM:17;
let X, Y be Element of bool M; :: according to CLOSURE1:def 3 :: thesis: ( X c= Y implies (P ** R) .. X c= (P ** R) .. Y )
assume X c= Y ; :: thesis: (P ** R) .. X c= (P ** R) .. Y
then R .. X c= R .. Y by A2, Def3;
then P .. (R .. X) c= P .. (R .. Y) by A1, Def3;
then P .. (R .. X) c= (P ** R) .. Y by A3, Th4, MSSUBFAM:12;
hence (P ** R) .. X c= (P ** R) .. Y by A3, Th4, MSSUBFAM:12; :: thesis: verum