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 )
thus f is monotonic ; :: thesis: ( f is idempotent & f is topological )
thus f is idempotent ; :: thesis: f is topological
thus f is topological :: thesis: verum
proof
let X, Y be Element of Bool M; :: according to CLOSURE2:def 13 :: thesis: f . (X (\/) Y) = (f . X) (\/) (f . Y)
( X c= M & Y c= M ) by PBOOLE:def 18;
then X (\/) Y c= M by PBOOLE:16;
then X (\/) Y is ManySortedSubset of M by PBOOLE:def 18;
then X (\/) Y in Bool M by Def1;
hence f . (X (\/) Y) = X (\/) Y by FUNCT_1:18
.= (f . X) (\/) Y
.= (f . X) (\/) (f . Y) ;
:: thesis: verum
end;