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

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