let g be SetOp of M; :: thesis: ( g is topological implies g is monotonic )
assume A1: g is topological ; :: thesis: g is monotonic
let X, Y be Element of Bool M; :: according to CLOSURE2:def 13 :: thesis: ( X c=' Y implies g . X c=' g . Y )
assume A2: X c= Y ; :: thesis: g . X c=' g . Y
(g . X) \/ (g . Y) = g . (X \/ Y) by A1, Def15
.= g . Y by A2, PBOOLE:24 ;
hence g . X c=' g . Y by PBOOLE:28; :: thesis: verum