reconsider f = id (Bool M) as SetOp of M ;
take f ; :: thesis: ( f is reflexive & f is monotonic & f is idempotent & f is topological )
thus f is reflexive :: thesis: ( f is monotonic & f is idempotent & f is topological )

proof

let X be Element of Bool M; :: according to CLOSURE2:def 12 :: thesis: X c=' f . X
thus X c=' f . X by FUNCT_1:35; :: thesis: verum

end;

thus f is monotonic :: thesis: ( f is idempotent & f is topological )

proof

let X, Y be Element of Bool M; :: according to CLOSURE2:def 13 :: thesis: ( X c=' Y implies f . X c=' f . Y )
assume A1: X c= Y ; :: thesis: f . X c=' f . Y
f . X = X by FUNCT_1:35;
hence f . X c=' f . Y by A1, FUNCT_1:35; :: thesis: verum

end;

thus f is idempotent :: thesis: f is topological

proof

let X be Element of Bool M; :: according to CLOSURE2:def 14 :: thesis: f . X = f . (f . X)
thus f . (f . X) = f . X by FUNCT_1:35; :: thesis: verum

end;

thus f is topological :: thesis: verum

proof

let X, Y be Element of Bool M; :: according to CLOSURE2:def 15 :: thesis: f . (X \/ Y) = (f . X) \/ (f . Y)
( X c= M & Y c= M ) by PBOOLE:def 23;
then X \/ Y c= M by PBOOLE:18;
then X \/ Y is ManySortedSubset of M by PBOOLE:def 23;
then X \/ Y in Bool M by Def1;
hence f . (X \/ Y) = X \/ Y by FUNCT_1:35
.= (f . X) \/ Y by FUNCT_1:35
.= (f . X) \/ (f . Y) by FUNCT_1:35 ;
:: thesis: verum

end;