reconsider I = the carrier of S as non empty set ;
set SS = ClSys->ClOp (SubAlgCl MA);
set M = the Sorts of (SubAlgCl MA);
let x be Element of Bool the Sorts of (SubAlgCl MA); :: according to CLOSURE3:def 3,CLOSURE3:def 4 :: thesis: ( x = (ClSys->ClOp (SubAlgCl MA)) . x implies ex A being SubsetFamily of the Sorts of (SubAlgCl MA) st
( A = { ((ClSys->ClOp (SubAlgCl MA)) . a) where a is Element of Bool the Sorts of (SubAlgCl MA) : ( a is finite-yielding & supp a is finite & a c= x ) } & x = MSUnion A ) )
assume A1: x = (ClSys->ClOp (SubAlgCl MA)) . x ; :: thesis: ex A being SubsetFamily of the Sorts of (SubAlgCl MA) st
( A = { ((ClSys->ClOp (SubAlgCl MA)) . a) where a is Element of Bool the Sorts of (SubAlgCl MA) : ( a is finite-yielding & supp a is finite & a c= x ) } & x = MSUnion A )
set A = { ((ClSys->ClOp (SubAlgCl MA)) . a) where a is Element of Bool the Sorts of (SubAlgCl MA) : ( a is finite-yielding & supp a is finite & a c= x ) } ;
{ ((ClSys->ClOp (SubAlgCl MA)) . a) where a is Element of Bool the Sorts of (SubAlgCl MA) : ( a is finite-yielding & supp a is finite & a c= x ) } c= Bool the Sorts of (SubAlgCl MA)

proof

let v be set ; :: according to TARSKI:def 3 :: thesis: ( not v in { ((ClSys->ClOp (SubAlgCl MA)) . a) where a is Element of Bool the Sorts of (SubAlgCl MA) : ( a is finite-yielding & supp a is finite & a c= x ) } or v in Bool the Sorts of (SubAlgCl MA) )
assume v in { ((ClSys->ClOp (SubAlgCl MA)) . a) where a is Element of Bool the Sorts of (SubAlgCl MA) : ( a is finite-yielding & supp a is finite & a c= x ) } ; :: thesis: v in Bool the Sorts of (SubAlgCl MA)
then ex a being Element of Bool the Sorts of (SubAlgCl MA) st
( v = (ClSys->ClOp (SubAlgCl MA)) . a & a is finite-yielding & supp a is finite & a c= x ) ;
then reconsider vv = v as Element of Bool the Sorts of (SubAlgCl MA) ;
vv in Bool the Sorts of (SubAlgCl MA) ;
hence v in Bool the Sorts of (SubAlgCl MA) ; :: thesis: verum

end;

then reconsider A = { ((ClSys->ClOp (SubAlgCl MA)) . a) where a is Element of Bool the Sorts of (SubAlgCl MA) : ( a is finite-yielding & supp a is finite & a c= x ) } as SubsetFamily of the Sorts of (SubAlgCl MA) ;
take A ; :: thesis: ( A = { ((ClSys->ClOp (SubAlgCl MA)) . a) where a is Element of Bool the Sorts of (SubAlgCl MA) : ( a is finite-yielding & supp a is finite & a c= x ) } & x = MSUnion A )
thus A = { ((ClSys->ClOp (SubAlgCl MA)) . b) where b is Element of Bool the Sorts of (SubAlgCl MA) : ( b is finite-yielding & supp b is finite & b c= x ) } ; :: thesis: x = MSUnion A
for i being set st i in I holds
x . i c= (MSUnion A) . i

proof

reconsider SS9 = ClSys->ClOp (SubAlgCl MA) as reflexive SetOp of the Sorts of (SubAlgCl MA) ;
let i be set ; :: thesis: ( i in I implies x . i c= (MSUnion A) . i )
assume A2: i in I ; :: thesis: x . i c= (MSUnion A) . i
let v be set ; :: according to TARSKI:def 3 :: thesis: ( not v in x . i or v in (MSUnion A) . i )
assume v in x . i ; :: thesis: v in (MSUnion A) . i
then consider b being Element of Bool the Sorts of (SubAlgCl MA) such that
A3: v in b . i and
A4: ( b is finite-yielding & supp b is finite & b c= x ) by A2, Th9;
b c=' SS9 . b by CLOSURE2:def 10;
then A5: b . i c= (SS9 . b) . i by A2, PBOOLE:def 2;
(ClSys->ClOp (SubAlgCl MA)) . b in A by A4;
then (SS9 . b) . i in { (f . i) where f is Element of Bool the Sorts of (SubAlgCl MA) : f in A } ;
then v in union { (f . i) where f is Element of Bool the Sorts of (SubAlgCl MA) : f in A } by A3, A5, TARSKI:def 4;
hence v in (MSUnion A) . i by A2, Def4; :: thesis: verum

end;

hence x c= MSUnion A by PBOOLE:def 2; :: according to PBOOLE:def 10 :: thesis: MSUnion A c= x
for i being set st i in I holds
(MSUnion A) . i c= x . i

proof

let i be set ; :: thesis: ( i in I implies (MSUnion A) . i c= x . i )
assume A6: 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

reconsider SS9 = ClSys->ClOp (SubAlgCl MA) as monotonic SetOp of the Sorts of (SubAlgCl MA) ;
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 the Sorts of (SubAlgCl MA) : ff in A } by A6, Def4;
then consider Y being set such that
A7: v in Y and
A8: Y in { (ff . i) where ff is Element of Bool the Sorts of (SubAlgCl MA) : ff in A } by TARSKI:def 4;
consider ff being Element of Bool the Sorts of (SubAlgCl MA) such that
A9: Y = ff . i and
A10: ff in A by A8;
consider a being Element of Bool the Sorts of (SubAlgCl MA) such that
A11: ff = (ClSys->ClOp (SubAlgCl MA)) . a and
a is finite-yielding and
supp a is finite and
A12: a c=' x by A10;
SS9 . a c=' SS9 . x by A12, CLOSURE2:def 11;
then ff . i c= x . i by A1, A6, A11, PBOOLE:def 2;
hence v in x . i by A7, A9; :: thesis: verum

end;

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

end;

hence MSUnion A c= x by PBOOLE:def 2; :: thesis: verum