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)

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

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

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) ;
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;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

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

hence
x = MSUnion A
; :: thesis: verum
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

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;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

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 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;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

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