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

proof

let x be Element of Bool M; :: according to CLOSURE3:def 3 :: thesis: ( x = f . x implies ex A being SubsetFamily of M st
( A = { (f . a) where a is Element of Bool M : ( a is finite-yielding & support a is finite & a c= x ) } & x = MSUnion A ) )
assume x = f . x ; :: thesis: ex A being SubsetFamily of M st
( A = { (f . a) where a is Element of Bool M : ( a is finite-yielding & support a is finite & a c= x ) } & x = MSUnion A )
set A = { (f . a) where a is Element of Bool M : ( a is finite-yielding & support a is finite & a c= x ) } ;
{ (f . a) where a is Element of Bool M : ( a is finite-yielding & support a is finite & a c= x ) } c= Bool M

proof

let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in { (f . a) where a is Element of Bool M : ( a is finite-yielding & support a is finite & a c= x ) } or v in Bool M )
assume v in { (f . a) where a is Element of Bool M : ( a is finite-yielding & support a is finite & a c= x ) } ; :: thesis: v in Bool M
then ex a being Element of Bool M st
( v = f . a & a is finite-yielding & support a is finite & a c= x ) ;
hence v in Bool M ; :: thesis: verum

end;

then reconsider A = { (f . a) where a is Element of Bool M : ( a is finite-yielding & support a is finite & a c= x ) } as SubsetFamily of M ;
take A ; :: thesis: ( A = { (f . a) where a is Element of Bool M : ( a is finite-yielding & support a is finite & a c= x ) } & x = MSUnion A )
thus A = { (f . a) where a is Element of Bool M : ( a is finite-yielding & support a is finite & a c= x ) } ; :: thesis: x = MSUnion A
let i be Element of I; :: according to PBOOLE:def 21 :: thesis: x . i = (MSUnion A) . i
thus x . i c= (MSUnion A) . i :: according to XBOOLE_0:def 10 :: thesis: (MSUnion A) . i c= x . i

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in x . i or y in (MSUnion A) . i )
assume y in x . i ; :: thesis: y in (MSUnion A) . i
then consider a being Element of Bool M such that
A1: y in a . i and
A2: ( a is finite-yielding & support a is finite & a c= x ) by Th7;
a = f . a ;
then a in A by A2;
then a . i in { (g . i) where g is Element of Bool M : g in A } ;
then y in union { (g . i) where g is Element of Bool M : g in A } by A1, TARSKI:def 4;
hence y in (MSUnion A) . i by Def2; :: thesis: verum

end;

let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in (MSUnion A) . i or v in x . i )
assume v in (MSUnion A) . i ; :: thesis: v in x . i
then v in union { (ff . i) where ff is Element of Bool M : ff in A } by Def2;
then consider Y being set such that
A3: v in Y and
A4: Y in { (ff . i) where ff is Element of Bool M : ff in A } by TARSKI:def 4;
consider ff being Element of Bool M such that
A5: Y = ff . i and
A6: ff in A by A4;
consider a being Element of Bool M such that
A7: ff = f . a and
a is finite-yielding and
support a is finite and
A8: a c= x by A6;
ff = a by A7;
then ff . i c= x . i by A8;
hence v in x . i by A3, A5; :: thesis: verum

end;

thus f is reflexive ; :: thesis: ( f is monotonic & f is idempotent )
thus f is monotonic ; :: thesis: f is idempotent
thus f is idempotent ; :: thesis: verum