let I be set ; :: thesis: for M being ManySortedSet of
for g, h being SetOp of M st g is monotonic & h is monotonic holds
g * h is monotonic
let M be ManySortedSet of ; :: thesis: for g, h being SetOp of M st g is monotonic & h is monotonic holds
g * h is monotonic
let g, h be SetOp of M; :: thesis: ( g is monotonic & h is monotonic implies g * h is monotonic )
assume that
A1: g is monotonic and
A2: h is monotonic ; :: thesis: g * h is monotonic
let X, Y be Element of Bool M; :: according to CLOSURE2:def 13 :: thesis: ( X c=' Y implies (g * h) . X c=' (g * h) . Y )
assume A3: X c= Y ; :: thesis: (g * h) . X c=' (g * h) . Y
A4: dom h = Bool M by FUNCT_2:def 1;
h . X c= h . Y by A2, A3, Def13;
then g . (h . X) c= g . (h . Y) by A1, Def13;
then g . (h . X) c= (g * h) . Y by A4, FUNCT_1:23;
hence (g * h) . X c=' (g * h) . Y by A4, FUNCT_1:23; :: thesis: verum