:: CLOSURE3 semantic presentation

begin

registration
let S be non empty 1-sorted ;
cluster 1-sorted(# the carrier of S #) ->  non empty ;
coherence
 not 1-sorted(# the carrier of S #) is empty ;
end;

theorem Th1: :: CLOSURE3:1
for I being non empty set
for M, N being ManySortedSet of I holds M +* N = N
proof
let I be non empty set ; ::_thesis: for M, N being ManySortedSet of I holds M +* N = N
let M, N be ManySortedSet of I; ::_thesis: M +* N = N
dom M = I by PARTFUN1:def_2
.= dom N by PARTFUN1:def_2 ;
hence  M +* N = N by FUNCT_4:19; ::_thesis: verum
end;

theorem :: CLOSURE3:2
for I being set
for M, N being ManySortedSet of I
for F being SubsetFamily of M st N in F holds
meet |:F:| c=' N by CLOSURE2:21, MSSUBFAM:43;

theorem Th3: :: CLOSURE3:3
for S being non empty non void ManySortedSign
for MA being strict non-empty MSAlgebra over S
for F being SubsetFamily of the Sorts of MA st F c= SubSort MA holds
for B being MSSubset of MA st B = meet |:F:| holds
B is opers_closed
proof
let S be non empty non void ManySortedSign ; ::_thesis: for MA being strict non-empty MSAlgebra over S
for F being SubsetFamily of the Sorts of MA st F c= SubSort MA holds
for B being MSSubset of MA st B = meet |:F:| holds
B is opers_closed
let MA be strict non-empty MSAlgebra over S; ::_thesis: for F being SubsetFamily of the Sorts of MA st F c= SubSort MA holds
for B being MSSubset of MA st B = meet |:F:| holds
B is opers_closed
let F be SubsetFamily of the Sorts of MA; ::_thesis: ( F c= SubSort MA implies for B being MSSubset of MA st B = meet |:F:| holds
B is opers_closed )
assume A1: F c= SubSort MA ; ::_thesis: for B being MSSubset of MA st B = meet |:F:| holds
B is opers_closed
let B be MSSubset of MA; ::_thesis: ( B = meet |:F:| implies B is opers_closed )
assume A2: B = meet |:F:| ; ::_thesis: B is opers_closed
percases ( F = {} or F <> {} ) ;
supposeA3: F = {} ; ::_thesis: B is opers_closed
set Q = the Sorts of MA;
reconsider FF = |:F:| as MSSubsetFamily of the Sorts of MA ;
set I = the carrier of S;
 FF = [[0]] the carrier of S by A3, CLOSURE2:def_3;
then A4: the Sorts of MA = B by A2, MSSUBFAM:41;
reconsider Q = the Sorts of MA as MSSubset of MA by PBOOLE:def_18;
 for o being OperSymbol of S holds Q is_closed_on o
proof
let o be OperSymbol of S; ::_thesis: Q is_closed_on o
A5: ( the ResultSort of S . o = the_result_sort_of o & dom the ResultSort of S = the carrier' of S ) by FUNCT_2:def_1, MSUALG_1:def_2;
Result (o,MA) = (Q * the ResultSort of S) . o by MSUALG_1:def_5
.= Q . (the_result_sort_of o) by A5, FUNCT_1:13 ;
then A6: rng ((Den (o,MA)) | ((Q #) . (the_arity_of o))) c= Q . (the_result_sort_of o) by RELAT_1:def_19;
 ( the Arity of S . o = the_arity_of o & dom the Arity of S = the carrier' of S ) by FUNCT_2:def_1, MSUALG_1:def_1;
then A7: ((Q #) * the Arity of S) . o = (Q #) . (the_arity_of o) by FUNCT_1:13;
 (Q * the ResultSort of S) . o = Q . (the_result_sort_of o) by A5, FUNCT_1:13;
hence  Q is_closed_on o by A7, A6, MSUALG_2:def_5; ::_thesis: verum
end;
hence  B is opers_closed by A4, MSUALG_2:def_6; ::_thesis: verum
end;
supposeA8: F <> {} ; ::_thesis: B is opers_closed
set SS = S;
let o be OperSymbol of S; :: according to MSUALG_2:def_6 ::_thesis: B is_closed_on o
set i = the_result_sort_of o;
A9: the ResultSort of S . o = the_result_sort_of o by MSUALG_1:def_2;
A10: dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1;
 ( the Arity of S . o = the_arity_of o & dom the Arity of S = the carrier' of S ) by FUNCT_2:def_1, MSUALG_1:def_1;
then A11: ((B #) * the Arity of S) . o = (B #) . (the_arity_of o) by FUNCT_1:13;
Result (o,MA) = ( the Sorts of MA * the ResultSort of S) . o by MSUALG_1:def_5
.= the Sorts of MA . (the_result_sort_of o) by A9, A10, FUNCT_1:13 ;
then A12: rng ((Den (o,MA)) | ((B #) . (the_arity_of o))) c= the Sorts of MA . (the_result_sort_of o) by RELAT_1:def_19;
A13: rng ((Den (o,MA)) | ((B #) . (the_arity_of o))) c= B . (the_result_sort_of o)
proof
consider Q being Subset-Family of ( the Sorts of MA . (the_result_sort_of o)) such that
A14: Q = |:F:| . (the_result_sort_of o) and
A15: B . (the_result_sort_of o) = Intersect Q by A2, MSSUBFAM:def_1;
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in rng ((Den (o,MA)) | ((B #) . (the_arity_of o))) or v in B . (the_result_sort_of o) )
assume A16: v in rng ((Den (o,MA)) | ((B #) . (the_arity_of o))) ; ::_thesis: v in B . (the_result_sort_of o)
then consider p being set  such that
A17: p in dom ((Den (o,MA)) | ((B #) . (the_arity_of o))) and
A18: v = ((Den (o,MA)) | ((B #) . (the_arity_of o))) . p by FUNCT_1:def_3;
 for Y being set st Y in Q holds
v in Y
proof
A19: |:F:| . (the_result_sort_of o) =  {  (xx . (the_result_sort_of o)) where xx is Element of Bool the Sorts of MA : xx in F  }  by A8, CLOSURE2:14;
let Y be set ; ::_thesis: ( Y in Q implies v in Y )
assume  Y in Q ; ::_thesis: v in Y
then consider xx being Element of Bool the Sorts of MA such that
A20: Y = xx . (the_result_sort_of o) and
A21: xx in F by A14, A19;
reconsider xx = xx as MSSubset of MA ;
 xx is opers_closed by A1, A21, MSUALG_2:14;
then  xx is_closed_on o by MSUALG_2:def_6;
then A22: rng ((Den (o,MA)) | (((xx #) * the Arity of S) . o)) c= (xx * the ResultSort of S) . o by MSUALG_2:def_5;
 B c= xx by A2, A21, CLOSURE2:21, MSSUBFAM:43;
then  (Den (o,MA)) | (((B #) * the Arity of S) . o) c= (Den (o,MA)) | (((xx #) * the Arity of S) . o) by MSUALG_2:2, RELAT_1:75;
then A23: dom ((Den (o,MA)) | (((B #) * the Arity of S) . o)) c= dom ((Den (o,MA)) | (((xx #) * the Arity of S) . o)) by RELAT_1:11;
A24: v = (Den (o,MA)) . p by A17, A18, FUNCT_1:47;
then  v = ((Den (o,MA)) | (((xx #) * the Arity of S) . o)) . p by A11, A17, A23, FUNCT_1:47;
then  v in rng ((Den (o,MA)) | (((xx #) * the Arity of S) . o)) by A11, A17, A23, FUNCT_1:def_3;
then  (Den (o,MA)) . p in (xx * the ResultSort of S) . o by A22, A24;
then  (Den (o,MA)) . p in xx . ( the ResultSort of S . o) by A10, FUNCT_1:13;
then  (Den (o,MA)) . p in xx . (the_result_sort_of o) by MSUALG_1:def_2;
hence  v in Y by A17, A18, A20, FUNCT_1:47; ::_thesis: verum
end;
hence  v in B . (the_result_sort_of o) by A12, A16, A15, SETFAM_1:43; ::_thesis: verum
end;
 (B * the ResultSort of S) . o = B . (the_result_sort_of o) by A9, A10, FUNCT_1:13;
hence  B is_closed_on o by A11, A13, MSUALG_2:def_5; ::_thesis: verum
end;
end;
end;

begin

theorem :: CLOSURE3:4
for A, B, C being set st A is_coarser_than B & B is_coarser_than C holds
A is_coarser_than C
proof
let A, B, C be set ; ::_thesis: ( A is_coarser_than B & B is_coarser_than C implies A is_coarser_than C )
assume that
A1: A is_coarser_than B and
A2: B is_coarser_than C ; ::_thesis: A is_coarser_than C
let a be set ; :: according to SETFAM_1:def_3 ::_thesis: ( not a in A or ex b1 being set st
( b1 in C & b1 c= a ) )
assume  a in A ; ::_thesis: ex b1 being set st
( b1 in C & b1 c= a )
then consider b being set  such that
A3: b in B and
A4: b c= a by A1, SETFAM_1:def_3;
consider c being set  such that
A5: ( c in C & c c= b ) by A2, A3, SETFAM_1:def_3;
take  c ; ::_thesis: ( c in C & c c= a )
thus  ( c in C & c c= a ) by A4, A5, XBOOLE_1:1; ::_thesis: verum
end;

LM: now__::_thesis:_for_I_being_non_empty_set_
for_M_being_ManySortedSet_of_I_holds_support_M_=__{__x_where_x_is_Element_of_I_:_M_._x_<>_{}__}_
let I be non empty set ; ::_thesis: for M being ManySortedSet of I holds support M =  {  x where x is Element of I : M . x <> {}  }
let M be ManySortedSet of I; ::_thesis: support M =  {  x where x is Element of I : M . x <> {}  }
set F =  {  x where x is Element of I : M . x <> {}  }  ;
thus  support M =  {  x where x is Element of I : M . x <> {}  }  ::_thesis: verum
proof
thus  support M c=  {  x where x is Element of I : M . x <> {}  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  x where x is Element of I : M . x <> {}  }  c= support M
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support M or x in  {  x where x is Element of I : M . x <> {}  }  )
A1: dom M = I by PARTFUN1:def_2;
A2: support M c= dom M by PRE_POLY:37;
assume A3: x in support M ; ::_thesis: x in  {  x where x is Element of I : M . x <> {}  }
then  M . x <> {} by PRE_POLY:def_7;
hence  x in  {  x where x is Element of I : M . x <> {}  }  by A1, A2, A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  x where x is Element of I : M . x <> {}  }  or x in support M )
assume  x in  {  x where x is Element of I : M . x <> {}  }  ; ::_thesis: x in support M
then  ex i being Element of I st
( x = i & M . i <> {} ) ;
hence  x in support M by PRE_POLY:def_7; ::_thesis: verum
end;
end;

definition
let I be non empty set ;
let M be ManySortedSet of I;
:: original: support
redefine func support M ->  set  equals :: CLOSURE3:def 1
 {  x where x is Element of I : M . x <> {}  }  ;
compatibility
 for b1 being set holds
( b1 = support M iff b1 =  {  x where x is Element of I : M . x <> {}  }  ) by LM;
end;

:: deftheorem  defines support CLOSURE3:def_1_:_
 for I being non empty set
for M being ManySortedSet of I holds support M =  {  x where x is Element of I : M . x <> {}  }  ;

theorem :: CLOSURE3:5
for I being non empty set
for M being V8() ManySortedSet of I holds M = ([[0]] I) +* (M | (support M))
proof
let I be non empty set ; ::_thesis: for M being V8() ManySortedSet of I holds M = ([[0]] I) +* (M | (support M))
let M be V8() ManySortedSet of I; ::_thesis: M = ([[0]] I) +* (M | (support M))
set MM = M | (support M);
A1: I c= support M
proof
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in I or v in support M )
assume A2: v in I ; ::_thesis: v in support M
then  M . v <> {} ;
hence  v in support M by A2; ::_thesis: verum
end;
 dom M = I by PARTFUN1:def_2;
then  M | (support M) = M by A1, RELAT_1:68;
hence  M = ([[0]] I) +* (M | (support M)) by Th1; ::_thesis: verum
end;

theorem :: CLOSURE3:6
for I being non empty set
for M1, M2 being V8() ManySortedSet of I st M1 | (support M1) = M2 | (support M2) holds
M1 = M2
proof
let I be non empty set ; ::_thesis: for M1, M2 being V8() ManySortedSet of I st M1 | (support M1) = M2 | (support M2) holds
M1 = M2
let M1, M2 be V8() ManySortedSet of I; ::_thesis: ( M1 | (support M1) = M2 | (support M2) implies M1 = M2 )
A1: dom M1 = I by PARTFUN1:def_2;
A2: dom M2 = I by PARTFUN1:def_2;
assume A3: M1 | (support M1) = M2 | (support M2) ; ::_thesis: M1 = M2
 for x being set st x in I holds
M1 . x = M2 . x
proof
let x be set ; ::_thesis: ( x in I implies M1 . x = M2 . x )
A4: dom (M2 | (support M2)) = (dom M2) /\ (support M2) by RELAT_1:61;
assume A5: x in I ; ::_thesis: M1 . x = M2 . x
then  not M1 . x is empty ;
then A6: x in support M1 by A5;
 not M2 . x is empty by A5;
then  x in support M2 by A5;
then A7: x in dom (M2 | (support M2)) by A2, A5, A4, XBOOLE_0:def_4;
 dom (M1 | (support M1)) = (dom M1) /\ (support M1) by RELAT_1:61;
then  x in dom (M1 | (support M1)) by A1, A5, A6, XBOOLE_0:def_4;
then M1 . x = (M2 | (support M2)) . x by A3, FUNCT_1:47
.= M2 . x by A7, FUNCT_1:47 ;
hence  M1 . x = M2 . x ; ::_thesis: verum
end;
hence  M1 = M2 by A1, A2, FUNCT_1:2; ::_thesis: verum
end;

theorem :: CLOSURE3:7
canceled;

theorem Th8: :: CLOSURE3:8
for I being non empty set
for M being ManySortedSet of I
for x being Element of Bool M
for i being Element of I
for y being set st y in x . i holds
ex a being Element of Bool M st
( y in a . i & a is V42() & support a is finite & a c= x )
proof
let I be non empty set ; ::_thesis: for M being ManySortedSet of I
for x being Element of Bool M
for i being Element of I
for y being set st y in x . i holds
ex a being Element of Bool M st
( y in a . i & a is V42() & support a is finite & a c= x )
let M be ManySortedSet of I; ::_thesis: for x being Element of Bool M
for i being Element of I
for y being set st y in x . i holds
ex a being Element of Bool M st
( y in a . i & a is V42() & support a is finite & a c= x )
let x be Element of Bool M; ::_thesis: for i being Element of I
for y being set st y in x . i holds
ex a being Element of Bool M st
( y in a . i & a is V42() & support a is finite & a c= x )
let i be Element of I; ::_thesis: for y being set st y in x . i holds
ex a being Element of Bool M st
( y in a . i & a is V42() & support a is finite & a c= x )
let y be set ; ::_thesis: ( y in x . i implies ex a being Element of Bool M st
( y in a . i & a is V42() & support a is finite & a c= x ) )
assume A1: y in x . i ; ::_thesis: ex a being Element of Bool M st
( y in a . i & a is V42() & support a is finite & a c= x )
set N = {i} --> {y};
set A = ([[0]] I) +* ({i} --> {y});
A2: dom ({i} --> {y}) = {i} by FUNCOP_1:13;
then A3: i in dom ({i} --> {y}) by TARSKI:def_1;
then A4: ({i} --> {y}) . i = {y} by A2, FUNCOP_1:7;
then A5: (([[0]] I) +* ({i} --> {y})) . i = {y} by A3, FUNCT_4:13;
A6: dom (([[0]] I) +* ({i} --> {y})) = (dom ([[0]] I)) \/ (dom ({i} --> {y})) by FUNCT_4:def_1
.= I \/ {i} by A2, PARTFUN1:def_2
.= I by ZFMISC_1:40 ;
then reconsider A = ([[0]] I) +* ({i} --> {y}) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
 for j being set st j in I holds
A . j c= M . j
proof
let j be set ; ::_thesis: ( j in I implies A . j c= M . j )
assume A7: j in I ; ::_thesis: A . j c= M . j
percases ( i = j or i <> j ) ;
supposeA8: i = j ; ::_thesis: A . j c= M . j
reconsider x = x as ManySortedSubset of M ;
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in A . j or v in M . j )
assume  v in A . j ; ::_thesis: v in M . j
then  v in {y} by A3, A4, A8, FUNCT_4:13;
then A9: v in x . j by A1, A8, TARSKI:def_1;
 x c= M by PBOOLE:def_18;
then  x . j c= M . j by A7, PBOOLE:def_2;
hence  v in M . j by A9; ::_thesis: verum
end;
suppose i <> j ; ::_thesis: A . j c= M . j
then A10: not j in {i} by TARSKI:def_1;
 j in (dom ([[0]] I)) \/ (dom ({i} --> {y})) by A6, A7, FUNCT_4:def_1;
then A . j = (I --> {}) . j by A2, A10, FUNCT_4:def_1
.= {} by A7, FUNCOP_1:7 ;
hence  A . j c= M . j by XBOOLE_1:2; ::_thesis: verum
end;
end;
end;
then  A c= M by PBOOLE:def_2;
then reconsider AA = A as ManySortedSubset of M by PBOOLE:def_18;
reconsider a = AA as Element of Bool M by CLOSURE2:def_1;
A11: for j being set st j in I holds
a . j c= x . j
proof
let j be set ; ::_thesis: ( j in I implies a . j c= x . j )
assume A12: j in I ; ::_thesis: a . j c= x . j
percases ( i = j or j <> i ) ;
supposeA13: i = j ; ::_thesis: a . j c= x . j
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in a . j or v in x . j )
assume A14: v in a . j ; ::_thesis: v in x . j
 a . j = {y} by A3, A4, A13, FUNCT_4:13;
hence  v in x . j by A1, A13, A14, TARSKI:def_1; ::_thesis: verum
end;
suppose j <> i ; ::_thesis: a . j c= x . j
then A15: not j in {i} by TARSKI:def_1;
 j in (dom ([[0]] I)) \/ (dom ({i} --> {y})) by A6, A12, FUNCT_4:def_1;
then a . j = (I --> {}) . j by A2, A15, FUNCT_4:def_1
.= {} by A12, FUNCOP_1:7 ;
hence  a . j c= x . j by XBOOLE_1:2; ::_thesis: verum
end;
end;
end;
A16:  {  b where b is Element of I : a . b <> {}  }  = {i}
proof
thus   {  b where b is Element of I : a . b <> {}  }  c= {i} :: according to XBOOLE_0:def_10 ::_thesis: {i} c=  {  b where b is Element of I : a . b <> {}  }
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in  {  b where b is Element of I : a . b <> {}  }  or s in {i} )
assume  s in  {  b where b is Element of I : a . b <> {}  }  ; ::_thesis: s in {i}
then A17: ex b being Element of I st
( s = b & a . b <> {} ) ;
assume A18: not s in {i} ; ::_thesis: contradiction
reconsider s = s as Element of I by A17;
 s in dom a by A6;
then  s in (dom ([[0]] I)) \/ (dom ({i} --> {y})) by FUNCT_4:def_1;
then a . s = (I --> {}) . s by A2, A18, FUNCT_4:def_1
.= {} by FUNCOP_1:7 ;
hence  contradiction by A17; ::_thesis: verum
end;
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in {i} or s in  {  b where b is Element of I : a . b <> {}  }  )
assume A19: s in {i} ; ::_thesis: s in  {  b where b is Element of I : a . b <> {}  }
then A20: s = i by TARSKI:def_1;
reconsider s = s as Element of I by A19, TARSKI:def_1;
 a . s = {y} by A3, A4, A20, FUNCT_4:13;
hence  s in  {  b where b is Element of I : a . b <> {}  }  ; ::_thesis: verum
end;
take  a ; ::_thesis: ( y in a . i & a is V42() & support a is finite & a c= x )
 for j being set st j in I holds
a . j is finite
proof
let j be set ; ::_thesis: ( j in I implies a . j is finite )
assume A21: j in I ; ::_thesis: a . j is finite
percases ( j = i or j <> i ) ;
suppose j = i ; ::_thesis: a . j is finite
hence  a . j is finite by A3, A4, FUNCT_4:13; ::_thesis: verum
end;
suppose j <> i ; ::_thesis: a . j is finite
then A22: not j in {i} by TARSKI:def_1;
 j in (dom ([[0]] I)) \/ (dom ({i} --> {y})) by A6, A21, FUNCT_4:def_1;
then a . j = (I --> {}) . j by A2, A22, FUNCT_4:def_1
.= {} by A21, FUNCOP_1:7 ;
hence  a . j is finite ; ::_thesis: verum
end;
end;
end;
hence  ( y in a . i & a is V42() & support a is finite & a c= x ) by A5, A16, A11, FINSET_1:def_5, PBOOLE:def_2, TARSKI:def_1; ::_thesis: verum
end;

definition
let I be set ;
let M be ManySortedSet of I;
let A be SubsetFamily of M;
func MSUnion A ->  ManySortedSubset of M means :Def2: :: CLOSURE3:def 2
 for i being set st i in I holds
it . i = union  {  (f . i) where f is Element of Bool M : f in A  }  ;
existence
 ex b1 being ManySortedSubset of M st
for i being set st i in I holds
b1 . i = union  {  (f . i) where f is Element of Bool M : f in A  }
proof
defpred S1[ set , set ] means $2 = union  {  (f . $1) where f is Element of Bool M : f in A  }  ;
A1: for x being set st x in I holds
ex y being set st S1[x,y] ;
consider IT being Function such that
A2: dom IT = I and
A3: for x being set st x in I holds
S1[x,IT . x] from CLASSES1:sch_1(A1);
reconsider IT = IT as ManySortedSet of I by A2, PARTFUN1:def_2, RELAT_1:def_18;
 for i being set st i in I holds
IT . i c= M . i
proof
let i be set ; ::_thesis: ( i in I implies IT . i c= M . i )
assume A4: i in I ; ::_thesis: IT . i c= M . i
 for x being set st x in IT . i holds
x in M . i
proof
let x be set ; ::_thesis: ( x in IT . i implies x in M . i )
assume A5: x in IT . i ; ::_thesis: x in M . i
 IT . i = union  {  (f . i) where f is Element of Bool M : f in A  }  by A3, A4;
then consider Y being set  such that
A6: x in Y and
A7: Y in  {  (f . i) where f is Element of Bool M : f in A  }  by A5, TARSKI:def_4;
consider ff being Element of Bool M such that
A8: ff . i = Y and
 ff in A by A7;
reconsider ff = ff as ManySortedSubset of M ;
 ff c= M by PBOOLE:def_18;
then  ff . i c= M . i by A4, PBOOLE:def_2;
hence  x in M . i by A6, A8; ::_thesis: verum
end;
hence  IT . i c= M . i by TARSKI:def_3; ::_thesis: verum
end;
then  IT c= M by PBOOLE:def_2;
then reconsider IT = IT as ManySortedSubset of M by PBOOLE:def_18;
take  IT ; ::_thesis: for i being set st i in I holds
IT . i = union  {  (f . i) where f is Element of Bool M : f in A  }
thus  for i being set st i in I holds
IT . i = union  {  (f . i) where f is Element of Bool M : f in A  }  by A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being ManySortedSubset of M st ( for i being set st i in I holds
b1 . i = union  {  (f . i) where f is Element of Bool M : f in A  }  ) & ( for i being set st i in I holds
b2 . i = union  {  (f . i) where f is Element of Bool M : f in A  }  ) holds
b1 = b2
proof
let B1, B2 be ManySortedSubset of M; ::_thesis: ( ( for i being set st i in I holds
B1 . i = union  {  (f . i) where f is Element of Bool M : f in A  }  ) & ( for i being set st i in I holds
B2 . i = union  {  (f . i) where f is Element of Bool M : f in A  }  ) implies B1 = B2 )
assume that
A9: for i being set st i in I holds
B1 . i = union  {  (f . i) where f is Element of Bool M : f in A  }  and
A10: for i being set st i in I holds
B2 . i = union  {  (ff . i) where ff is Element of Bool M : ff in A  }  ; ::_thesis: B1 = B2
 for i being set st i in I holds
B1 . i = B2 . i
proof
let i be set ; ::_thesis: ( i in I implies B1 . i = B2 . i )
assume A11: i in I ; ::_thesis: B1 . i = B2 . i
then B1 . i = union  {  (f . i) where f is Element of Bool M : f in A  }  by A9
.= B2 . i by A10, A11 ;
hence  B1 . i = B2 . i ; ::_thesis: verum
end;
hence  B1 = B2 by PBOOLE:3; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines MSUnion CLOSURE3:def_2_:_
 for I being set
for M being ManySortedSet of I
for A being SubsetFamily of M
for b4 being ManySortedSubset of M holds
( b4 = MSUnion A iff for i being set st i in I holds
b4 . i = union  {  (f . i) where f is Element of Bool M : f in A  }  );

registration
let I be set ;
let M be ManySortedSet of I;
let A be empty SubsetFamily of M;
cluster MSUnion A -> V9() ;
coherence
 MSUnion A is empty-yielding
proof
let i be set ; :: according to PBOOLE:def_12 ::_thesis: ( not i in I or (MSUnion A) . i is empty )
set MA = MSUnion A;
assume  i in I ; ::_thesis: (MSUnion A) . i is empty
then A1: (MSUnion A) . i = union  {  (f . i) where f is Element of Bool M : f in A  }  by Def2;
assume  not (MSUnion A) . i is empty ; ::_thesis: contradiction
then consider v being set  such that
A2: v in (MSUnion A) . i by XBOOLE_0:def_1;
consider h being set  such that
 v in h and
A3: h in  {  (f . i) where f is Element of Bool M : f in A  }  by A1, A2, TARSKI:def_4;
 ex g being Element of Bool M st
( h = g . i & g in A ) by A3;
hence  contradiction ; ::_thesis: verum
end;
end;

theorem :: CLOSURE3:9
for I being set
for M being ManySortedSet of I
for A being SubsetFamily of M holds MSUnion A = union |:A:|
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for A being SubsetFamily of M holds MSUnion A = union |:A:|
let M be ManySortedSet of I; ::_thesis: for A being SubsetFamily of M holds MSUnion A = union |:A:|
let A be SubsetFamily of M; ::_thesis: MSUnion A = union |:A:|
set AA = |:A:|;
reconsider UA = union |:A:| as ManySortedSet of I ;
percases ( not A is empty or A is empty SubsetFamily of M ) ;
supposeA1: not A is empty ; ::_thesis: MSUnion A = union |:A:|
 for i being set st i in I holds
(MSUnion A) . i = UA . i
proof
let i be set ; ::_thesis: ( i in I implies (MSUnion A) . i = UA . i )
assume A2: i in I ; ::_thesis: (MSUnion A) . i = UA . i
then  ( |:A:| . i =  {  (g . i) where g is Element of Bool M : g in A  }  & UA . i = union (|:A:| . i) ) by A1, CLOSURE2:14, MBOOLEAN:def_2;
hence  (MSUnion A) . i = UA . i by A2, Def2; ::_thesis: verum
end;
hence  MSUnion A = union |:A:| by PBOOLE:3; ::_thesis: verum
end;
supposeA3: A is empty SubsetFamily of M ; ::_thesis: MSUnion A = union |:A:|
 for i being set st i in I holds
(MSUnion A) . i = UA . i
proof
let i be set ; ::_thesis: ( i in I implies (MSUnion A) . i = UA . i )
assume  i in I ; ::_thesis: (MSUnion A) . i = UA . i
 |:A:| = [[0]] I by A3, CLOSURE2:def_3;
then  UA = [[0]] I by MBOOLEAN:21;
then  UA . i is empty ;
hence  (MSUnion A) . i = UA . i by A3; ::_thesis: verum
end;
hence  MSUnion A = union |:A:| by PBOOLE:3; ::_thesis: verum
end;
end;
end;

definition
let I be set ;
let M be ManySortedSet of I;
let A, B be SubsetFamily of M;
:: original: \/
redefine funcA \/ B ->  SubsetFamily of M;
correctness
coherence
A \/ B is SubsetFamily of M;
by CLOSURE2:3;
end;

theorem :: CLOSURE3:10
for I being set
for M being ManySortedSet of I
for A, B being SubsetFamily of M holds MSUnion (A \/ B) = (MSUnion A) \/ (MSUnion B)
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for A, B being SubsetFamily of M holds MSUnion (A \/ B) = (MSUnion A) \/ (MSUnion B)
let M be ManySortedSet of I; ::_thesis: for A, B being SubsetFamily of M holds MSUnion (A \/ B) = (MSUnion A) \/ (MSUnion B)
let A, B be SubsetFamily of M; ::_thesis: MSUnion (A \/ B) = (MSUnion A) \/ (MSUnion B)
reconsider MAB = MSUnion (A \/ B) as ManySortedSubset of M ;
reconsider MAB = MAB as ManySortedSet of I ;
reconsider MA = MSUnion A as ManySortedSubset of M ;
reconsider MA = MA as ManySortedSet of I ;
reconsider MB = MSUnion B as ManySortedSubset of M ;
reconsider MB = MB as ManySortedSet of I ;
 for i being set st i in I holds
MAB . i = (MA \/ MB) . i
proof
let i be set ; ::_thesis: ( i in I implies MAB . i = (MA \/ MB) . i )
assume A1: i in I ; ::_thesis: MAB . i = (MA \/ MB) . i
then A2: MAB . i = union  {  (f . i) where f is Element of Bool M : f in A \/ B  }  by Def2;
A3: (MA \/ MB) . i = (MA . i) \/ (MB . i) by A1, PBOOLE:def_4;
A4: for v being set st v in (MA \/ MB) . i holds
v in MAB . i
proof
let v be set ; ::_thesis: ( v in (MA \/ MB) . i implies v in MAB . i )
assume  v in (MA \/ MB) . i ; ::_thesis: v in MAB . i
then A5: ( v in MA . i or v in MB . i ) by A3, XBOOLE_0:def_3;
percases ( v in union  {  (f . i) where f is Element of Bool M : f in A  }  or v in union  {  (f . i) where f is Element of Bool M : f in B  }  ) by A1, A5, Def2;
suppose v in union  {  (f . i) where f is Element of Bool M : f in A  }  ; ::_thesis: v in MAB . i
then consider g being set  such that
A6: v in g and
A7: g in  {  (f . i) where f is Element of Bool M : f in A  }  by TARSKI:def_4;
consider h being Element of Bool M such that
A8: g = h . i and
A9: h in A by A7;
 h in A \/ B by A9, XBOOLE_0:def_3;
then  g in  {  (f . i) where f is Element of Bool M : f in A \/ B  }  by A8;
hence  v in MAB . i by A2, A6, TARSKI:def_4; ::_thesis: verum
end;
suppose v in union  {  (f . i) where f is Element of Bool M : f in B  }  ; ::_thesis: v in MAB . i
then consider g being set  such that
A10: v in g and
A11: g in  {  (f . i) where f is Element of Bool M : f in B  }  by TARSKI:def_4;
consider h being Element of Bool M such that
A12: g = h . i and
A13: h in B by A11;
 h in A \/ B by A13, XBOOLE_0:def_3;
then  g in  {  (f . i) where f is Element of Bool M : f in A \/ B  }  by A12;
hence  v in MAB . i by A2, A10, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
A14: ( MA . i = union  {  (f . i) where f is Element of Bool M : f in A  }  & MB . i = union  {  (f . i) where f is Element of Bool M : f in B  }  ) by A1, Def2;
 for v being set st v in MAB . i holds
v in (MA \/ MB) . i
proof
let v be set ; ::_thesis: ( v in MAB . i implies v in (MA \/ MB) . i )
assume  v in MAB . i ; ::_thesis: v in (MA \/ MB) . i
then consider h being set  such that
A15: v in h and
A16: h in  {  (f . i) where f is Element of Bool M : f in A \/ B  }  by A2, TARSKI:def_4;
consider g being Element of Bool M such that
A17: h = g . i and
A18: g in A \/ B by A16;
 ( g in A or g in B ) by A18, XBOOLE_0:def_3;
then  ( h in  {  (f . i) where f is Element of Bool M : f in A  }  or h in  {  (f . i) where f is Element of Bool M : f in B  }  ) by A17;
then  ( v in union  {  (f . i) where f is Element of Bool M : f in A  }  or v in union  {  (f . i) where f is Element of Bool M : f in B  }  ) by A15, TARSKI:def_4;
hence  v in (MA \/ MB) . i by A3, A14, XBOOLE_0:def_3; ::_thesis: verum
end;
hence  MAB . i = (MA \/ MB) . i by A4, TARSKI:1; ::_thesis: verum
end;
hence  MSUnion (A \/ B) = (MSUnion A) \/ (MSUnion B) by PBOOLE:3; ::_thesis: verum
end;

theorem :: CLOSURE3:11
for I being set
for M being ManySortedSet of I
for A, B being SubsetFamily of M st A c= B holds
MSUnion A c= MSUnion B
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for A, B being SubsetFamily of M st A c= B holds
MSUnion A c= MSUnion B
let M be ManySortedSet of I; ::_thesis: for A, B being SubsetFamily of M st A c= B holds
MSUnion A c= MSUnion B
let A, B be SubsetFamily of M; ::_thesis: ( A c= B implies MSUnion A c= MSUnion B )
reconsider MA = MSUnion A as ManySortedSubset of M ;
reconsider MA = MA as ManySortedSet of I ;
reconsider MB = MSUnion B as ManySortedSubset of M ;
reconsider MB = MB as ManySortedSet of I ;
assume A1: A c= B ; ::_thesis: MSUnion A c= MSUnion B
 for i being set st i in I holds
MA . i c= MB . i
proof
let i be set ; ::_thesis: ( i in I implies MA . i c= MB . i )
assume A2: i in I ; ::_thesis: MA . i c= MB . i
 for v being set st v in MA . i holds
v in MB . i
proof
A3: MA . i = union  {  (f . i) where f is Element of Bool M : f in A  }  by A2, Def2;
let v be set ; ::_thesis: ( v in MA . i implies v in MB . i )
assume  v in MA . i ; ::_thesis: v in MB . i
then consider h being set  such that
A4: v in h and
A5: h in  {  (f . i) where f is Element of Bool M : f in A  }  by A3, TARSKI:def_4;
 ex g being Element of Bool M st
( h = g . i & g in A ) by A5;
then  h in  {  (k . i) where k is Element of Bool M : k in B  }  by A1;
then  v in union  {  (k . i) where k is Element of Bool M : k in B  }  by A4, TARSKI:def_4;
hence  v in MB . i by A2, Def2; ::_thesis: verum
end;
hence  MA . i c= MB . i by TARSKI:def_3; ::_thesis: verum
end;
hence  MSUnion A c= MSUnion B by PBOOLE:def_2; ::_thesis: verum
end;

definition
let I be set ;
let M be ManySortedSet of I;
let A, B be SubsetFamily of M;
:: original: /\
redefine funcA /\ B ->  SubsetFamily of M;
correctness
coherence
A /\ B is SubsetFamily of M;
by CLOSURE2:4;
end;

theorem :: CLOSURE3:12
for I being set
for M being ManySortedSet of I
for A, B being SubsetFamily of M holds MSUnion (A /\ B) c= (MSUnion A) /\ (MSUnion B)
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for A, B being SubsetFamily of M holds MSUnion (A /\ B) c= (MSUnion A) /\ (MSUnion B)
let M be ManySortedSet of I; ::_thesis: for A, B being SubsetFamily of M holds MSUnion (A /\ B) c= (MSUnion A) /\ (MSUnion B)
let A, B be SubsetFamily of M; ::_thesis: MSUnion (A /\ B) c= (MSUnion A) /\ (MSUnion B)
reconsider MAB = MSUnion (A /\ B) as ManySortedSet of I ;
reconsider MA = MSUnion A as ManySortedSet of I ;
reconsider MB = MSUnion B as ManySortedSet of I ;
 for i being set st i in I holds
MAB . i c= (MA /\ MB) . i
proof
let i be set ; ::_thesis: ( i in I implies MAB . i c= (MA /\ MB) . i )
assume A1: i in I ; ::_thesis: MAB . i c= (MA /\ MB) . i
then A2: ( MA . i = union  {  (f . i) where f is Element of Bool M : f in A  }  & MB . i = union  {  (f . i) where f is Element of Bool M : f in B  }  ) by Def2;
A3: MAB . i = union  {  (f . i) where f is Element of Bool M : f in A /\ B  }  by A1, Def2;
 for v being set st v in MAB . i holds
v in (MA /\ MB) . i
proof
let v be set ; ::_thesis: ( v in MAB . i implies v in (MA /\ MB) . i )
assume  v in MAB . i ; ::_thesis: v in (MA /\ MB) . i
then consider w being set  such that
A4: v in w and
A5: w in  {  (f . i) where f is Element of Bool M : f in A /\ B  }  by A3, TARSKI:def_4;
consider g being Element of Bool M such that
A6: w = g . i and
A7: g in A /\ B by A5;
 g in B by A7, XBOOLE_0:def_4;
then  w in  {  (f . i) where f is Element of Bool M : f in B  }  by A6;
then A8: v in union  {  (f . i) where f is Element of Bool M : f in B  }  by A4, TARSKI:def_4;
 g in A by A7, XBOOLE_0:def_4;
then  w in  {  (f . i) where f is Element of Bool M : f in A  }  by A6;
then  v in union  {  (f . i) where f is Element of Bool M : f in A  }  by A4, TARSKI:def_4;
then  v in (MA . i) /\ (MB . i) by A2, A8, XBOOLE_0:def_4;
hence  v in (MA /\ MB) . i by A1, PBOOLE:def_5; ::_thesis: verum
end;
hence  MAB . i c= (MA /\ MB) . i by TARSKI:def_3; ::_thesis: verum
end;
hence  MSUnion (A /\ B) c= (MSUnion A) /\ (MSUnion B) by PBOOLE:def_2; ::_thesis: verum
end;

theorem :: CLOSURE3:13
for I being set
for M being ManySortedSet of I
for AA being set st ( for x being set st x in AA holds
x is SubsetFamily of M ) holds
for A, B being SubsetFamily of M st B =  {  (MSUnion X) where X is SubsetFamily of M : X in AA  }  & A = union AA holds
MSUnion B = MSUnion A
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for AA being set st ( for x being set st x in AA holds
x is SubsetFamily of M ) holds
for A, B being SubsetFamily of M st B =  {  (MSUnion X) where X is SubsetFamily of M : X in AA  }  & A = union AA holds
MSUnion B = MSUnion A
let M be ManySortedSet of I; ::_thesis: for AA being set st ( for x being set st x in AA holds
x is SubsetFamily of M ) holds
for A, B being SubsetFamily of M st B =  {  (MSUnion X) where X is SubsetFamily of M : X in AA  }  & A = union AA holds
MSUnion B = MSUnion A
let AA be set ; ::_thesis: ( ( for x being set st x in AA holds
x is SubsetFamily of M ) implies for A, B being SubsetFamily of M st B =  {  (MSUnion X) where X is SubsetFamily of M : X in AA  }  & A = union AA holds
MSUnion B = MSUnion A )
assume A1: for x being set st x in AA holds
x is SubsetFamily of M ; ::_thesis: for A, B being SubsetFamily of M st B =  {  (MSUnion X) where X is SubsetFamily of M : X in AA  }  & A = union AA holds
MSUnion B = MSUnion A
let A, B be SubsetFamily of M; ::_thesis: ( B =  {  (MSUnion X) where X is SubsetFamily of M : X in AA  }  & A = union AA implies MSUnion B = MSUnion A )
assume that
A2: B =  {  (MSUnion X) where X is SubsetFamily of M : X in AA  }  and
A3: A = union AA ; ::_thesis: MSUnion B = MSUnion A
let i be set ; :: according to PBOOLE:def_10 ::_thesis: ( not i in I or (MSUnion B) . i = (MSUnion A) . i )
assume A4: i in I ; ::_thesis: (MSUnion B) . i = (MSUnion A) . i
thus  (MSUnion B) . i c= (MSUnion A) . i :: according to XBOOLE_0:def_10 ::_thesis: (MSUnion A) . i c= (MSUnion B) . i
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (MSUnion B) . i or a in (MSUnion A) . i )
thus  ( a in (MSUnion B) . i implies a in (MSUnion A) . i ) ::_thesis: verum
proof
assume  a in (MSUnion B) . i ; ::_thesis: a in (MSUnion A) . i
then  a in union  {  (f . i) where f is Element of Bool M : f in B  }  by A4, Def2;
then consider Y being set  such that
A5: a in Y and
A6: Y in  {  (f . i) where f is Element of Bool M : f in B  }  by TARSKI:def_4;
consider f being Element of Bool M such that
A7: f . i = Y and
A8: f in B by A6;
consider Q being SubsetFamily of M such that
A9: f = MSUnion Q and
A10: Q in AA by A2, A8;
 (MSUnion Q) . i = union  {  (g . i) where g is Element of Bool M : g in Q  }  by A4, Def2;
then consider d being set  such that
A11: a in d and
A12: d in  {  (g . i) where g is Element of Bool M : g in Q  }  by A5, A7, A9, TARSKI:def_4;
consider g being Element of Bool M such that
A13: d = g . i and
A14: g in Q by A12;
 g in union AA by A10, A14, TARSKI:def_4;
then  d in  {  (h . i) where h is Element of Bool M : h in union AA  }  by A13;
then  a in union  {  (h . i) where h is Element of Bool M : h in union AA  }  by A11, TARSKI:def_4;
hence  a in (MSUnion A) . i by A3, A4, Def2; ::_thesis: verum
end;
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (MSUnion A) . i or a in (MSUnion B) . i )
assume  a in (MSUnion A) . i ; ::_thesis: a in (MSUnion B) . i
then  a in union  {  (f . i) where f is Element of Bool M : f in A  }  by A4, Def2;
then consider Y being set  such that
A15: a in Y and
A16: Y in  {  (f . i) where f is Element of Bool M : f in A  }  by TARSKI:def_4;
consider f being Element of Bool M such that
A17: f . i = Y and
A18: f in A by A16;
consider c being set  such that
A19: f in c and
A20: c in AA by A3, A18, TARSKI:def_4;
reconsider c = c as SubsetFamily of M by A1, A20;
 f . i in  {  (v . i) where v is Element of Bool M : v in c  }  by A19;
then A21: a in union  {  (v . i) where v is Element of Bool M : v in c  }  by A15, A17, TARSKI:def_4;
 (MSUnion c) . i = union  {  (v . i) where v is Element of Bool M : v in c  }  by A4, Def2;
then consider cos being set  such that
A22: a in cos and
A23: cos = (MSUnion c) . i by A21;
 MSUnion c in  {  (MSUnion X) where X is SubsetFamily of M : X in AA  }  by A20;
then  cos in  {  (t . i) where t is Element of Bool M : t in B  }  by A2, A23;
then  a in union  {  (t . i) where t is Element of Bool M : t in B  }  by A22, TARSKI:def_4;
hence  a in (MSUnion B) . i by A4, Def2; ::_thesis: verum
end;

begin

definition
let I be non empty set ;
let M be ManySortedSet of I;
let S be SetOp of M;
attrS is algebraic  means :: CLOSURE3:def 3
 for x being Element of Bool M st x = S . x holds
ex A being SubsetFamily of M st
( A =  {  (S . a) where a is Element of Bool M : ( a is V42() & support a is finite & a c= x )  }  & x = MSUnion A );
end;

:: deftheorem  defines algebraic CLOSURE3:def_3_:_
 for I being non empty set
for M being ManySortedSet of I
for S being SetOp of M holds
( S is algebraic iff for x being Element of Bool M st x = S . x holds
ex A being SubsetFamily of M st
( A =  {  (S . a) where a is Element of Bool M : ( a is V42() & support a is finite & a c= x )  }  & x = MSUnion A ) );

registration
let I be non empty set ;
let M be ManySortedSet of I;
cluster non empty Relation-like Bool M -defined Bool M -valued Function-like V17( Bool M) quasi_total reflexive monotonic idempotent algebraic for Element of bool [:(Bool M),(Bool M):];
existence
 ex b1 being SetOp of M st
( b1 is algebraic & b1 is reflexive & b1 is monotonic & b1 is idempotent )
proof
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 V42() & 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 V42() & support a is finite & a c= x )  }  & x = MSUnion A )
set A =  {  (f . a) where a is Element of Bool M : ( a is V42() & support a is finite & a c= x )  }  ;
  {  (f . a) where a is Element of Bool M : ( a is V42() & support 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 V42() & 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 V42() & 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 V42() & 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 V42() & 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 V42() & support a is finite & a c= x )  }  & x = MSUnion A )
thus  A =  {  (f . a) where a is Element of Bool M : ( a is V42() & 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 set ; :: 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 V42() & support a is finite & a c= x ) by Th8;
 a = f . a by FUNCT_1:18;
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 set ; :: 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 V42() and
 support a is finite and
A8: a c= x by A6;
 ff = a by A7, FUNCT_1:18;
then  ff . i c= x . i by A8, PBOOLE:def_2;
hence  v in x . i by A3, A5; ::_thesis: verum
end;
thus  f is reflexive ::_thesis: ( f is monotonic & f is idempotent )
proof
let X be Element of Bool M; :: according to CLOSURE2:def_10 ::_thesis: X c= f . X
thus  X c= f . X by FUNCT_1:18; ::_thesis: verum
end;
thus  f is monotonic ::_thesis: f is idempotent
proof
let X, Y be Element of Bool M; :: according to CLOSURE2:def_11 ::_thesis: ( not X c= Y or f . X c= f . Y )
assume A9: X c= Y ; ::_thesis: f . X c= f . Y
 f . X = X by FUNCT_1:18;
hence  f . X c= f . Y by A9, FUNCT_1:18; ::_thesis: verum
end;
thus  f is idempotent ::_thesis: verum
proof
let X be Element of Bool M; :: according to CLOSURE2:def_12 ::_thesis: f . X = f . (f . X)
thus  f . (f . X) = f . X by FUNCT_1:18; ::_thesis: verum
end;
end;
end;

definition
let S be non empty 1-sorted ;
let IT be ClosureSystem of S;
attrIT is algebraic  means :: CLOSURE3:def 4
 ClSys->ClOp IT is algebraic ;
end;

:: deftheorem  defines algebraic CLOSURE3:def_4_:_
 for S being non empty 1-sorted
for IT being ClosureSystem of S holds
( IT is algebraic iff ClSys->ClOp IT is algebraic );

definition
let S be non empty non void ManySortedSign ;
let MA be non-empty MSAlgebra over S;
func SubAlgCl MA ->  strict ClosureStr over 1-sorted(# the carrier of S #) means :Def5: :: CLOSURE3:def 5
( the Sorts of it = the Sorts of MA & the Family of it = SubSort MA );
existence
 ex b1 being strict ClosureStr over 1-sorted(# the carrier of S #) st
( the Sorts of b1 = the Sorts of MA & the Family of b1 = SubSort MA )
proof
reconsider SS = the Sorts of MA as ManySortedSet of the carrier of 1-sorted(# the carrier of S #) ;
 SubSort MA c= Bool the Sorts of MA
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SubSort MA or x in Bool the Sorts of MA )
assume  x in SubSort MA ; ::_thesis: x in Bool the Sorts of MA
then  x is ManySortedSubset of the Sorts of MA by MSUALG_2:def_11;
hence  x in Bool the Sorts of MA by CLOSURE2:def_1; ::_thesis: verum
end;
then reconsider SF = SubSort MA as SubsetFamily of SS ;
take  ClosureStr(# SS,SF #) ; ::_thesis: ( the Sorts of ClosureStr(# SS,SF #) = the Sorts of MA & the Family of ClosureStr(# SS,SF #) = SubSort MA )
thus  ( the Sorts of ClosureStr(# SS,SF #) = the Sorts of MA & the Family of ClosureStr(# SS,SF #) = SubSort MA ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict ClosureStr over 1-sorted(# the carrier of S #) st the Sorts of b1 = the Sorts of MA & the Family of b1 = SubSort MA & the Sorts of b2 = the Sorts of MA & the Family of b2 = SubSort MA holds
b1 = b2 ;
end;

:: deftheorem Def5 defines SubAlgCl CLOSURE3:def_5_:_
 for S being non empty non void ManySortedSign
for MA being non-empty MSAlgebra over S
for b3 being strict ClosureStr over 1-sorted(# the carrier of S #) holds
( b3 = SubAlgCl MA iff ( the Sorts of b3 = the Sorts of MA & the Family of b3 = SubSort MA ) );

theorem Th14: :: CLOSURE3:14
for S being non empty non void ManySortedSign
for MA being strict non-empty MSAlgebra over S holds SubSort MA is absolutely-multiplicative SubsetFamily of the Sorts of MA
proof
let S be non empty non void ManySortedSign ; ::_thesis: for MA being strict non-empty MSAlgebra over S holds SubSort MA is absolutely-multiplicative SubsetFamily of the Sorts of MA
let MA be strict non-empty MSAlgebra over S; ::_thesis: SubSort MA is absolutely-multiplicative SubsetFamily of the Sorts of MA
 SubSort MA c= Bool the Sorts of MA
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SubSort MA or x in Bool the Sorts of MA )
assume  x in SubSort MA ; ::_thesis: x in Bool the Sorts of MA
then  x is ManySortedSubset of the Sorts of MA by MSUALG_2:def_11;
hence  x in Bool the Sorts of MA by CLOSURE2:def_1; ::_thesis: verum
end;
then reconsider SUBMA = SubSort MA as SubsetFamily of the Sorts of MA ;
 for F being SubsetFamily of the Sorts of MA st F c= SUBMA holds
meet |:F:| in SUBMA
proof
set M = bool (Union the Sorts of MA);
set I = the carrier of S;
let F be SubsetFamily of the Sorts of MA; ::_thesis: ( F c= SUBMA implies meet |:F:| in SUBMA )
assume A1: F c= SUBMA ; ::_thesis: meet |:F:| in SUBMA
set x = meet |:F:|;
A2: dom (meet |:F:|) = the carrier of S by PARTFUN1:def_2;
 rng (meet |:F:|) c= bool (Union the Sorts of MA)
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in rng (meet |:F:|) or u in bool (Union the Sorts of MA) )
assume  u in rng (meet |:F:|) ; ::_thesis: u in bool (Union the Sorts of MA)
then consider i being set  such that
A3: i in dom (meet |:F:|) and
A4: u = (meet |:F:|) . i by FUNCT_1:def_3;
 dom the Sorts of MA = the carrier of S by PARTFUN1:def_2;
then  the Sorts of MA . i in rng the Sorts of MA by A2, A3, FUNCT_1:def_3;
then A5: the Sorts of MA . i c= union (rng the Sorts of MA) by ZFMISC_1:74;
 ex Q being Subset-Family of ( the Sorts of MA . i) st
( Q = |:F:| . i & u = Intersect Q ) by A2, A3, A4, MSSUBFAM:def_1;
then  u c= union (rng the Sorts of MA) by A5, XBOOLE_1:1;
then  u in bool (union (rng the Sorts of MA)) ;
hence  u in bool (Union the Sorts of MA) by CARD_3:def_4; ::_thesis: verum
end;
then A6: meet |:F:| in Funcs ( the carrier of S,(bool (Union the Sorts of MA))) by A2, FUNCT_2:def_2;
reconsider x = meet |:F:| as MSSubset of MA ;
 for B being MSSubset of MA st B = x holds
B is opers_closed by A1, Th3;
hence  meet |:F:| in SUBMA by A6, MSUALG_2:def_11; ::_thesis: verum
end;
hence  SubSort MA is absolutely-multiplicative SubsetFamily of the Sorts of MA by CLOSURE2:def_7; ::_thesis: verum
end;

registration
let S be non empty non void ManySortedSign ;
let MA be strict non-empty MSAlgebra over S;
cluster SubAlgCl MA ->  strict absolutely-multiplicative ;
coherence
 SubAlgCl MA is absolutely-multiplicative
proof
thus  SubAlgCl MA is absolutely-multiplicative ::_thesis: verum
proof
reconsider SF = SubSort MA as absolutely-multiplicative SubsetFamily of the Sorts of MA by Th14;
set F = the Family of (SubAlgCl MA);
 ( the Sorts of (SubAlgCl MA) = the Sorts of MA & the Family of (SubAlgCl MA) = SF ) by Def5;
hence  SubAlgCl MA is absolutely-multiplicative ; ::_thesis: verum
end;
end;
end;

registration
let S be non empty non void ManySortedSign ;
let MA be strict non-empty MSAlgebra over S;
cluster SubAlgCl MA ->  strict algebraic ;
coherence
 SubAlgCl MA is algebraic
proof
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 V42() & 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 V42() & 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 V42() & 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 V42() & support 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 V42() & 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 V42() & 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 V42() & 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 V42() & 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 V42() & 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 V42() & 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 set ; :: 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 V42() & support b is finite & b c= x ) by Th8;
 b c=' SS9 . b by CLOSURE2:def_10;
then A4: b . i c= (SS9 . b) . i by PBOOLE:def_2;
 (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 set ; :: 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 V42() 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, PBOOLE:def_2;
hence  v in y . i by A5, A7; ::_thesis: verum
end;
hence  x = MSUnion A ; ::_thesis: verum
end;
end;