let P be MSSetOp of M; :: thesis: ( P is topological implies P is monotonic )
assume A1: P is topological ; :: thesis: P is monotonic
let X, Y be Element of bool M; :: according to CLOSURE1:def 2 :: thesis: ( X c= Y implies P .. X c= P .. Y )
assume A2: X c= Y ; :: thesis: P .. X c= P .. Y
(P .. X) (\/) (P .. Y) = P .. (X (\/) Y) by A1
.= P .. Y by A2, PBOOLE:22 ;
hence P .. X c= P .. Y by PBOOLE:26; :: thesis: verum