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 by Th8; :: thesis: ( F is monotonic & F is idempotent & F is topological )
thus F is monotonic by Th9; :: thesis: ( F is idempotent & F is topological )
thus F is idempotent by Th8; :: thesis: F is topological
thus F is topological :: thesis: verum
proof
let X, Y be Element of bool M; :: according to CLOSURE1:def 4 :: thesis: F .. (X (\/) Y) = (F .. X) (\/) (F .. Y)
Y in bool M by MSSUBFAM:12;
then A1: Y c= M by MBOOLEAN:1;
X in bool M by MSSUBFAM:12;
then X c= M by MBOOLEAN:1;
then X (\/) Y c= M by A1, PBOOLE:16;
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;