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 5 :: 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 & supp 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 & supp a is finite & a c= x ) } & x = MSUnion A )
set A = { (f . a) where a is Element of Bool M : ( a is finite-yielding & supp a is finite & a c= x ) } ;
{ (f . a) where a is Element of Bool M : ( a is finite-yielding & supp a is finite & a c= x ) } c= Bool M

proof

let v be set ; :: according to TARSKI:def 3 :: thesis: ( not v in { (f . a) where a is Element of Bool M : ( a is finite-yielding & supp 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 & supp a is finite & a c= x ) } ; :: thesis: v in Bool M
then consider a being Element of Bool M such that
A1: v = f . a and
( a is finite-yielding & supp a is finite & a c= x ) ;
thus v in Bool M by A1; :: thesis: verum

end;

then reconsider A = { (f . a) where a is Element of Bool M : ( a is finite-yielding & supp 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 & supp a is finite & a c= x ) } & x = MSUnion A )
thus A = { (f . a) where a is Element of Bool M : ( a is finite-yielding & supp a is finite & a c= x ) } ; :: thesis: x = MSUnion A
thus x c= MSUnion A :: according to PBOOLE:def 13 :: thesis: MSUnion A c= x

proof

let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or x . i c= (MSUnion A) . i )
assume A2: i in I ; :: thesis: x . i c= (MSUnion A) . i
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in x . i or y in (MSUnion A) . i )
assume A3: y in x . i ; :: thesis: y in (MSUnion A) . i
consider a being Element of Bool M such that
A4: ( y in a . i & a is finite-yielding & supp a is finite & a c= x ) by A2, A3, Th9;
a = f . a by FUNCT_1:35;
then a in A by A4;
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 A4, TARSKI:def 4;
hence y in (MSUnion A) . i by A2, Def4; :: thesis: verum

end;

thus MSUnion A c= x :: thesis: verum

proof

let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or (MSUnion A) . i c= x . i )
assume A5: i in I ; :: thesis: (MSUnion A) . i c= x . i
for v being set st v in (MSUnion A) . i holds
v in x . i

proof

let v be set ; :: thesis: ( v in (MSUnion A) . i implies 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 A5, Def4;
then consider Y being set such that
A6: v in Y and
A7: 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
A8: Y = ff . i and
A9: ff in A by A7;
consider a being Element of Bool M such that
A10: ff = f . a and
A11: ( a is finite-yielding & supp a is finite & a c= x ) by A9;
ff = a by A10, FUNCT_1:35;
then ff . i c= x . i by A5, A11, PBOOLE:def 5;
hence v in x . i by A6, A8; :: thesis: verum

end;

hence (MSUnion A) . i c= x . i by TARSKI:def 3; :: thesis: verum

end;

end;

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

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

proof

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

end;

thus f is idempotent :: thesis: verum

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;