reconsider F = id (bool M) as MSSetOp 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 CLOSURE1:def 2 :: thesis: X c= F .. X
thus X c= F .. X by Th8; :: 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 CLOSURE1:def 3 :: thesis: ( X c= Y implies F .. X c= F .. Y )
assume X c= Y ; :: thesis: F .. X c= F .. Y
hence F .. X c= F .. Y by Th9; :: thesis: verum

end;

thus F is idempotent :: thesis: F is topological

proof

let X be Element of bool M; :: according to CLOSURE1:def 4 :: thesis: F .. X = F .. (F .. X)
thus F .. X = F .. (F .. X) by Th8; :: thesis: verum

end;

thus F is topological :: thesis: verum

proof

let X, Y be Element of bool M; :: according to CLOSURE1:def 5 :: thesis: F .. (X \/ Y) = (F .. X) \/ (F .. Y)
( X in bool M & Y in bool M ) by MSSUBFAM:12;
then ( X c= M & Y c= M ) by MBOOLEAN:1;
then X \/ Y c= M by PBOOLE:18;
then X \/ Y in bool M by MBOOLEAN:1;
then X \/ Y is Element of bool M by MSSUBFAM:11;
hence F .. (X \/ Y) = (F .. X) \/ (F .. Y) by Th10; :: thesis: verum

end;