set I = the carrier of S;
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 V45() & support 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 V45() & support 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 V45() & support a is finite & a c= x ) } ;
{ ((ClSys->ClOp (SubAlgCl MA)) . a) where a is Element of Bool the Sorts of (SubAlgCl MA) : ( a is V45() & support a is finite & a c= x ) } c= Bool the Sorts of (SubAlgCl MA)
proof
let v be object ; :: 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 V45() & support 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 V45() & support 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 V45() & support 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 V45() & support 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 V45() & support 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 V45() & support b is finite & b c= x ) } ; :: thesis: x = MSUnion A
reconsider y = x, z = MSUnion A as ManySortedSet of the carrier of S ;
y = z
proof
let i be Element of the carrier of S; :: according to PBOOLE:def 21 :: thesis: y . i = z . i
reconsider SS9 = ClSys->ClOp (SubAlgCl MA) as reflexive SetOp of the Sorts of (SubAlgCl MA) ;
thus y . i c= z . i :: according to XBOOLE_0:def 10 :: thesis: z . i c= y . i
proof
let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in y . i or v in z . i )
assume v in y . i ; :: thesis: v in z . i
then consider b being Element of Bool the Sorts of (SubAlgCl MA) such that
A2: v in b . i and
A3: ( b is V45() & support b is finite & b c= x ) by Th7;
b c=' SS9 . b by CLOSURE2:def 10;
then A4: b . i c= (SS9 . b) . i ;
(ClSys->ClOp (SubAlgCl MA)) . b in A by A3;
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 A2, A4, TARSKI:def 4;
hence v in z . i by Def2; :: thesis: verum
end;
reconsider SS9 = ClSys->ClOp (SubAlgCl MA) as monotonic SetOp of the Sorts of (SubAlgCl MA) ;
let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in z . i or v in y . i )
assume v in z . i ; :: thesis: v in y . i
then v in union { (ff . i) where ff is Element of Bool the Sorts of (SubAlgCl MA) : ff in A } by Def2;
then consider Y being set such that
A5: v in Y and
A6: 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
A7: Y = ff . i and
A8: ff in A by A6;
consider a being Element of Bool the Sorts of (SubAlgCl MA) such that
A9: ff = (ClSys->ClOp (SubAlgCl MA)) . a and
a is V45() and
support a is finite and
A10: a c=' x by A8;
SS9 . a c=' SS9 . x by A10, CLOSURE2:def 11;
then ff . i c= x . i by A1, A9;
hence v in y . i by A5, A7; :: thesis: verum
end;
hence x = MSUnion A ; :: thesis: verum