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 11 :: 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
.= g . Y by A2, PBOOLE:22 ;
hence g . X c=' g . Y by PBOOLE:26; :: thesis: verum